Theorem ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016) (Proof shortened by Wolf Lammen, 22-Jan-2025)

	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		alinexa	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
5	1	nfn	⊢ Ⅎ 𝑥 ¬ 𝜓
6	3	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
7	5 2 6	ceqsal	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ¬ 𝜑 ) ↔ ¬ 𝜓 )
8	4 7	bitr3i	⊢ ( ¬ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ¬ 𝜓 )
9	8	con4bii	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜓 )