Assume H1: ∃z ∈ X, P z.

We will prove (x ∈ (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) → x ∈ X ∧ P x).

We prove the intermediate claim L1: (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) = {F x|x ∈ X}.

An exact proof term for the current goal is (If_i_1 (∃z ∈ X, P z) {F x|x ∈ X} Empty H1).

rewrite the current goal using L1 (from left to right).

We will prove x ∈ {F x|x ∈ X} → x ∈ X ∧ P x.

Assume H2: x ∈ {F x|x ∈ X}.

Apply (ReplE_impred X F x H2) to the current goal.

Let y be given.

Assume H3: y ∈ X.

Assume H4: x = F y.

We will prove x ∈ X ∧ P x.

Apply (xm (P y)) to the current goal.

Assume H5: P y.

We prove the intermediate claim L2: x = y.

rewrite the current goal using (If_i_1 (P y) y z H5) (from right to left).

An exact proof term for the current goal is H4.

rewrite the current goal using L2 (from left to right).

We will prove y ∈ X ∧ P y.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is H5.

Assume H5: ¬ P y.

We prove the intermediate claim L2: x = z.

rewrite the current goal using (If_i_0 (P y) y z H5) (from right to left).

An exact proof term for the current goal is H4.

rewrite the current goal using L2 (from left to right).

We will prove z ∈ X ∧ P z.

An exact proof term for the current goal is (Eps_i_ex (λz ⇒ z ∈ X ∧ P z) H1).

Assume H1: ¬ ∃z ∈ X, P z.

We will prove (x ∈ (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) → x ∈ X ∧ P x).

We prove the intermediate claim L1: (if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty) = Empty.

An exact proof term for the current goal is (If_i_0 (∃z ∈ X, P z) {F x|x ∈ X} Empty H1).

rewrite the current goal using L1 (from left to right).

We will prove x ∈ Empty → x ∈ X ∧ P x.

Assume H2: x ∈ Empty.

We will prove False.

An exact proof term for the current goal is (EmptyE x H2).