Let X, P and x be given.
Set z to be the term Eps_i (λz ⇒ z ∈ X ∧ P z) of type set.
Set F to be the term λx ⇒ if P x then x else z of type set → set.
Assume H1: x ∈ X.
Assume H2: P x.
We prove the intermediate claim L1: ∃z ∈ X, P z.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is H2.
We will prove x ∈ {x ∈ X|P x}.
We will prove x ∈ if (∃z ∈ X, P z) then {F x|x ∈ X} else Empty.
We prove the intermediate claim L2: (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 L1).
rewrite the current goal using L2 (from left to right).
We will prove x ∈ {F x|x ∈ X}.
We prove the intermediate claim L3: F x = x.
We will prove (if P x then x else z) = x.
An exact proof term for the current goal is (If_i_1 (P x) x z H2).
rewrite the current goal using L3 (from right to left).
We will prove F x ∈ {F x|x ∈ X}.
An exact proof term for the current goal is (ReplI X F x H1).
∎