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

Metamath Proof Explorer

Theorem eqvincf

Description: A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003)

		Ref	Expression
	Hypotheses	eqvincf.1	⊢ Ⅎ 𝑥 𝐴
		eqvincf.2	⊢ Ⅎ 𝑥 𝐵
		eqvincf.3	⊢ 𝐴 ∈ V
	Assertion	eqvincf	⊢ ( 𝐴 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqvincf.1	⊢ Ⅎ 𝑥 𝐴
2		eqvincf.2	⊢ Ⅎ 𝑥 𝐵
3		eqvincf.3	⊢ 𝐴 ∈ V
4	3	eqvinc	⊢ ( 𝐴 = 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = 𝐵 ) )
5	1	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
6	2	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐵
7	5 6	nfan	⊢ Ⅎ 𝑥 ( 𝑦 = 𝐴 ∧ 𝑦 = 𝐵 )
8		nfv	⊢ Ⅎ 𝑦 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 )
9		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝐴 ↔ 𝑥 = 𝐴 ) )
10		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = 𝐵 ↔ 𝑥 = 𝐵 ) )
11	9 10	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
12	7 8 11	cbvexv1	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) )
13	4 12	bitri	⊢ ( 𝐴 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) )