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 ⊢ Ⅎ _ x A
eqvincf.2 ⊢ Ⅎ _ x B
eqvincf.3 ⊢ A ∈ V
Assertion eqvincf ⊢ A = B ↔ ∃ x x = A ∧ x = B

Proof

Step Hyp Ref Expression
1 eqvincf.1 ⊢ Ⅎ _ x A
2 eqvincf.2 ⊢ Ⅎ _ x B
3 eqvincf.3 ⊢ A ∈ V
4 3 eqvinc ⊢ A = B ↔ ∃ y y = A ∧ y = B
5 1 nfeq2 ⊢ Ⅎ x y = A
6 2 nfeq2 ⊢ Ⅎ x y = B
7 5 6 nfan ⊢ Ⅎ x y = A ∧ y = B
8 nfv ⊢ Ⅎ y x = A ∧ x = B
9 eqeq1 ⊢ y = x → y = A ↔ x = A
10 eqeq1 ⊢ y = x → y = B ↔ x = B
11 9 10 anbi12d ⊢ y = x → y = A ∧ y = B ↔ x = A ∧ x = B
12 7 8 11 cbvexv1 ⊢ ∃ y y = A ∧ y = B ↔ ∃ x x = A ∧ x = B
13 4 12 bitri ⊢ A = B ↔ ∃ x x = A ∧ x = B