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

Metamath Proof Explorer

Theorem eqvincg

Description: A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017)

Ref Expression
Assertion eqvincg ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elisset ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )
2 ax-1 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 = 𝐵 → 𝑥 = 𝐴 ) )
3 eqtr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝐴 = 𝐵 ) → 𝑥 = 𝐵 )
4 3 ex ⊢ ( 𝑥 = 𝐴 → ( 𝐴 = 𝐵 → 𝑥 = 𝐵 ) )
5 2 4 jca ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 = 𝐵 → 𝑥 = 𝐴 ) ∧ ( 𝐴 = 𝐵 → 𝑥 = 𝐵 ) ) )
6 5 eximi ⊢ ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( ( 𝐴 = 𝐵 → 𝑥 = 𝐴 ) ∧ ( 𝐴 = 𝐵 → 𝑥 = 𝐵 ) ) )
7 pm3.43 ⊢ ( ( ( 𝐴 = 𝐵 → 𝑥 = 𝐴 ) ∧ ( 𝐴 = 𝐵 → 𝑥 = 𝐵 ) ) → ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
8 7 eximi ⊢ ( ∃ 𝑥 ( ( 𝐴 = 𝐵 → 𝑥 = 𝐴 ) ∧ ( 𝐴 = 𝐵 → 𝑥 = 𝐵 ) ) → ∃ 𝑥 ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
9 1 6 8 3syl ⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
10 19.37v ⊢ ( ∃ 𝑥 ( 𝐴 = 𝐵 → ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) ↔ ( 𝐴 = 𝐵 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
11 9 10 sylib ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )
12 eqtr2 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → 𝐴 = 𝐵 )
13 12 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) → 𝐴 = 𝐵 )
14 11 13 impbid1 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐵 ) ) )