Theorem ceqex

Description: Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995) (Proof shortened by BJ, 1-May-2019)

	Ref	Expression
Assertion	ceqex	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
2	1	ex	⊢ ( 𝑥 = 𝐴 → ( 𝜑 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
3		eqvisset	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
4		alexeqg	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
5	3 4	syl	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
6		sp	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → ( 𝑥 = 𝐴 → 𝜑 ) )
7	6	com12	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) → 𝜑 ) )
8	5 7	sylbird	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
9	2 8	impbid	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )