This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alexeqg

Description: Two ways to express substitution of A for x in ph . This is the analogue for classes of sbalex . (Contributed by NM, 2-Mar-1995) (Revised by BJ, 27-Apr-2019)

		Ref	Expression
	Assertion	alexeqg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
2	1	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
3	2	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4	1	imbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜑 ) ) )
5	4	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
6		sbalex	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
7	3 5 6	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
8	7	bicomd	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )