Let x0 of type ι be given.
Let x1 of type (ι → ο) → ο be given.
Let x2 of type (ι → ο) → ο be given.
Assume H0:
∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ x4 ∈ x0) ⟶ iff (x1 x3) (x2 x3).
Apply set_ext with
{x3 ∈ prim4 x0|x1 (λ x4 . x4 ∈ x3)},
{x3 ∈ prim4 x0|x2 (λ x4 . x4 ∈ x3)} leaving 2 subgoals.
Let x3 of type ι be given.
Assume H1:
x3 ∈ {x4 ∈ prim4 x0|x1 (λ x5 . x5 ∈ x4)}.
Apply SepE with
prim4 x0,
λ x4 . x1 (λ x5 . x5 ∈ x4),
x3,
x3 ∈ {x4 ∈ prim4 x0|x2 (λ x5 . x5 ∈ x4)} leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
x3 ∈ prim4 x0.
Assume H3: x1 (λ x4 . x4 ∈ x3).
Apply SepI with
prim4 x0,
λ x4 . x2 (λ x5 . x5 ∈ x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H0 with
λ x4 . x4 ∈ x3,
x2 (λ x4 . x4 ∈ x3) leaving 2 subgoals.
Apply PowerE with
x0,
x3.
The subproof is completed by applying H2.
Assume H4: x1 (λ x4 . x4 ∈ x3) ⟶ x2 (λ x4 . x4 ∈ x3).
Assume H5: x2 (λ x4 . x4 ∈ x3) ⟶ x1 (λ x4 . x4 ∈ x3).
Apply H4.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H1:
x3 ∈ {x4 ∈ prim4 x0|x2 (λ x5 . x5 ∈ x4)}.
Apply SepE with
prim4 x0,
λ x4 . x2 (λ x5 . x5 ∈ x4),
x3,
x3 ∈ {x4 ∈ prim4 x0|x1 (λ x5 . x5 ∈ x4)} leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2:
x3 ∈ prim4 x0.
Assume H3: x2 (λ x4 . x4 ∈ x3).
Apply SepI with
prim4 x0,
λ x4 . x1 (λ x5 . x5 ∈ x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H0 with
λ x4 . x4 ∈ x3,
x1 (λ x4 . x4 ∈ x3) leaving 2 subgoals.
Apply PowerE with
x0,
x3.
The subproof is completed by applying H2.
Assume H4: x1 (λ x4 . x4 ∈ x3) ⟶ x2 (λ x4 . x4 ∈ x3).
Assume H5: x2 (λ x4 . x4 ∈ x3) ⟶ x1 (λ x4 . x4 ∈ x3).
Apply H5.
The subproof is completed by applying H3.