Theorem ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016)

	Ref	Expression
Hypotheses	ceqsex.1	⊢ Ⅎ 𝑥 𝜓
	ceqsex.2	⊢ 𝐴 ∈ V
	ceqsex.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	ceqsex	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ceqsex.1	⊢ Ⅎ 𝑥 𝜓
2		ceqsex.2	⊢ 𝐴 ∈ V
3		ceqsex.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4	3	biimpa	⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝜓 )
5	1 4	exlimi	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝜓 )
6	3	biimprcd	⊢ ( 𝜓 → ( 𝑥 = 𝐴 → 𝜑 ) )
7	1 6	alrimi	⊢ ( 𝜓 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) )
8	2	isseti	⊢ ∃ 𝑥 𝑥 = 𝐴
9		exintr	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
10	7 8 9	mpisyl	⊢ ( 𝜓 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
11	5 10	impbii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 )