Theorem eqvinc 1407

Description: A variable introduction law for class equality.

Hypothesis

Ref	Expression
eqvinc.1	|- A e. V

Assertion

Ref	Expression
eqvinc	|- (A = B <-> E.x(x = A /\ x = B))

Distinct variable group(s):   x,A   x,B

Proof of Theorem eqvinc

Step	Hyp	Ref	Expression
1		eqvinc.1	. . 3 |- A e. V
2		eleq1 1149	. . 3 |- (A = B -> (A e. V <-> B e. V))
3	1, 2	mpbii 168	. 2 |- (A = B -> B e. V)
4		visset 1350	. . . . 5 |- x e. V
5		eleq1 1149	. . . . 5 |- (x = B -> (x e. V <-> B e. V))
6	4, 5	mpbii 168	. . . 4 |- (x = B -> B e. V)
7	6	adantl 305	. . 3 |- ((x = A /\ x = B) -> B e. V)
8	7	19.23aiv 952	. 2 |- (E.x(x = A /\ x = B) -> B e. V)
9		cleq2 1110	. . 3 |- (z = B -> (A = z <-> A = B))
10		cleq2 1110	. . . . 5 |- (z = B -> (x = z <-> x = B))
11	10	anbi2d 468	. . . 4 |- (z = B -> ((x = A /\ x = z) <-> (x = A /\ x = B)))
12	11	biexdv 936	. . 3 |- (z = B -> (E.x(x = A /\ x = z) <-> E.x(x = A /\ x = B)))
13		cleq1 1107	. . . 4 |- (y = A -> (y = z <-> A = z))
14		cleq1 1107	. . . . . . 7 |- (y = A -> (y = x <-> A = x))
15		cleqcom 1103	. . . . . . 7 |- (A = x <-> x = A)
16	14, 15	syl6bb 414	. . . . . 6 |- (y = A -> (y = x <-> x = A))
17	16	anbi1d 469	. . . . 5 |- (y = A -> ((y = x /\ x = z) <-> (x = A /\ x = z)))
18	17	biexdv 936	. . . 4 |- (y = A -> (E.x(y = x /\ x = z) <-> E.x(x = A /\ x = z)))
19		eqvin 932	. . . 4 |- (y = z <-> E.x(y = x /\ x = z))
20	1, 13, 18, 19	vtoclb 1381	. . 3 |- (A = z <-> E.x(x = A /\ x = z))
21	9, 12, 20	vtoclbg 1384	. 2 |- (B e. V -> (A = B <-> E.x(x = A /\ x = B)))
22	3, 8, 21	pm5.21nii 504	1 |- (A = B <-> E.x(x = A /\ x = B))

Syntax hints:   <-> wb 127   /\ wa 196  E.wex 678   = weq 797   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  eqvincf 1408  opabid 2099  findsg 2398  tfindsg 2402  f1fv 2916  indpi 3828

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org