Theorem opeq2 3858

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	|- ( A = B -> <. C , A >. = <. C , B >. )

Proof of Theorem opeq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2292	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 464	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2230	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3744	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3751	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2299	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) ) )
8		df-3an 1004	. . . 4 |- ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) )
9		df-3an 1004	. . . 4 |- ( ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) )
11	10	abbidv 2347	. 2 |- ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } )
12		df-op 3675	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3675	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2287	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1002   = wceq 1395   e. wcel 2200   {cab 2215   _Vcvv 2799   {csn 3666   {cpr 3667   <.cop 3669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  opeq12  3859  opeq2i  3861  opeq2d  3864  oteq2  3867  oteq3  3868  breq2  4087  cbvopab2  4158  cbvopab2v  4161  opthg  4324  eqvinop  4329  opelopabsb  4348  opelxp  4749  opabid2  4853  elrn2g  4912  opeldm  4926  opeldmg  4928  elrn2  4966  opelresg  5012  iss  5051  elimasng  5096  issref  5111  dmsnopg  5200  cnvsng  5214  elxp4  5216  elxp5  5217  dffun5r  5330  funopg  5352  f1osng  5614  tz6.12f  5656  fsn  5807  fsng  5808  fvsng  5835  oveq2  6009  cbvoprab2  6077  ovg  6144  opabex3d  6266  opabex3  6267  op1stg  6296  op2ndg  6297  oprssdmm  6317  op1steq  6325  dfoprab4f  6339  tfrlemibxssdm  6473  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  elixpsn  6882  ixpsnf1o  6883  mapsnen  6964  xpsnen  6980  xpassen  6989  xpf1o  7005  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  djulclb  7222  inl11  7232  djuss  7237  1stinl  7241  2ndinl  7242  1stinr  7243  2ndinr  7244  elreal  8015  ax1rid  8064  fseq1p1m1  10290  pfxval  11206  swrdccatin1  11257  swrdccat3blem  11271  imasaddfnlemg  13347  cnmpt21  14965  djucllem  16164