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

Metamath Proof Explorer

Theorem eqvinc

Description: A variable introduction law for class equality. (Contributed by NM, 14-Apr-1995) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof shortened by Thierry Arnoux, 23-Jan-2022)

Ref Expression
Hypothesis eqvinc.1 ⊢ A ∈ V
Assertion eqvinc ⊢ A = B ↔ ∃ x x = A ∧ x = B

Proof

Step Hyp Ref Expression
1 eqvinc.1 ⊢ A ∈ V
2 eqvincg ⊢ A ∈ V → A = B ↔ ∃ x x = A ∧ x = B
3 1 2 ax-mp ⊢ A = B ↔ ∃ x x = A ∧ x = B