Theorem opeq1 3857

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

Assertion

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

Proof of Theorem opeq1

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	anbi1d 465	. . . . 5 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3677	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3743	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3751	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2299	. . . . 5 |- ( A = B -> ( x e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) ) )
8		df-3an 1004	. . . 4 |- ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) )
9		df-3an 1004	. . . 4 |- ( ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) ) )
11	10	abbidv 2347	. 2 |- ( A = B -> { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) } = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) } )
12		df-op 3675	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3675	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2287	1 |- ( A = B -> <. A , C >. = <. B , C >. )

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  opeq1i  3860  opeq1d  3863  oteq1  3866  breq1  4086  cbvopab1  4157  cbvopab1s  4159  opthg  4324  eqvinop  4329  opelopabsb  4348  opelxp  4749  elvvv  4782  opabid2  4853  opeliunxp2  4862  elsnres  5042  elimasng  5096  rnxpid  5163  dmsnopg  5200  cnvsng  5214  elxp4  5216  elxp5  5217  funopg  5352  f1osng  5614  dmfco  5702  fvelrn  5766  fsng  5808  fvsng  5835  funfvima3  5873  oveq1  6008  oprabid  6033  dfoprab2  6051  cbvoprab1  6076  opabex3d  6266  opabex3  6267  op1stg  6296  op2ndg  6297  oprssdmm  6317  dfoprab4f  6339  cnvoprab  6380  opeliunxp2f  6384  tfr1onlemaccex  6494  tfrcllemaccex  6507  elixpsn  6882  fundmen  6959  xpsnen  6980  xpassen  6989  xpf1o  7005  ltexnqq  7595  archnqq  7604  prarloclemarch2  7606  prarloclemlo  7681  prarloclem3  7684  prarloclem5  7687  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemdisj  7861  caucvgprlemloc  7862  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprlem1  7866  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemcbv  7874  caucvgprprlemval  7875  caucvgprprlemnkeqj  7877  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemlol  7885  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  caucvgprprlem1  7896  caucvgprprlem2  7897  caucvgsr  7989  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  suplocsr  7996  elrealeu  8016  pitonn  8035  nntopi  8081  axcaucvglemval  8084  axcaucvg  8087  axpre-suploclemres  8088  swrdccatin1  11257  swrdccat3blem  11271  fsum2dlemstep  11945  fprod2dlemstep  12133  imasaddfnlemg  13347  cnmpt21  14965