Theorem eqvincg 3648

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem eqvincg

Step	Hyp	Ref	Expression
1		elisset 2823	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴)
2		ax-1 6	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝐴 = 𝐵 → 𝑥 = 𝐴))
3		eqtr 2760	. . . . . . 7 ⊢ ((𝑥 = 𝐴 ∧ 𝐴 = 𝐵) → 𝑥 = 𝐵)
4	3	ex 412	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝐴 = 𝐵 → 𝑥 = 𝐵))
5	2, 4	jca 511	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)))
6	5	eximi 1835	. . . 4 ⊢ (∃𝑥 𝑥 = 𝐴 → ∃𝑥((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)))
7		pm3.43 473	. . . . 5 ⊢ (((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)) → (𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
8	7	eximi 1835	. . . 4 ⊢ (∃𝑥((𝐴 = 𝐵 → 𝑥 = 𝐴) ∧ (𝐴 = 𝐵 → 𝑥 = 𝐵)) → ∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
9	1, 6, 8	3syl 18	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
10		19.37v 1991	. . 3 ⊢ (∃𝑥(𝐴 = 𝐵 → (𝑥 = 𝐴 ∧ 𝑥 = 𝐵)) ↔ (𝐴 = 𝐵 → ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
11	9, 10	sylib 218	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 → ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))
12		eqtr2 2761	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → 𝐴 = 𝐵)
13	12	exlimiv 1930	. 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵) → 𝐴 = 𝐵)
14	11, 13	impbid1 225	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 = 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 = 𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  eqvinc  3649  funcnv5mpt  32678