Theorem opeq1 3858

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 3678	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3744	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3752	. . . . . 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 3676	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3676	. 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 2800   {csn 3667   {cpr 3668   <.cop 3670

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  opeq12  3860  opeq1i  3861  opeq1d  3864  oteq1  3867  breq1  4087  cbvopab1  4158  cbvopab1s  4160  opthg  4326  eqvinop  4331  opelopabsb  4350  opelxp  4751  elvvv  4785  opabid2  4857  opeliunxp2  4866  elsnres  5046  elimasng  5100  rnxpid  5167  dmsnopg  5204  cnvsng  5218  elxp4  5220  elxp5  5221  funopg  5356  f1osng  5620  dmfco  5708  fvelrn  5772  fsng  5814  fvsng  5843  funfvima3  5881  oveq1  6018  oprabid  6043  dfoprab2  6061  cbvoprab1  6086  opabex3d  6276  opabex3  6277  op1stg  6306  op2ndg  6307  oprssdmm  6327  dfoprab4f  6349  cnvoprab  6392  opeliunxp2f  6397  tfr1onlemaccex  6507  tfrcllemaccex  6520  elixpsn  6897  fundmen  6974  xpsnen  6998  xpassen  7007  xpf1o  7023  ltexnqq  7616  archnqq  7625  prarloclemarch2  7627  prarloclemlo  7702  prarloclem3  7705  prarloclem5  7708  caucvgprlemnkj  7874  caucvgprlemnbj  7875  caucvgprlemm  7876  caucvgprlemdisj  7882  caucvgprlemloc  7883  caucvgprlemcl  7884  caucvgprlemladdfu  7885  caucvgprlemladdrl  7886  caucvgprlem1  7887  caucvgprlem2  7888  caucvgpr  7890  caucvgprprlemell  7893  caucvgprprlemelu  7894  caucvgprprlemcbv  7895  caucvgprprlemval  7896  caucvgprprlemnkeqj  7898  caucvgprprlemmu  7903  caucvgprprlemopl  7905  caucvgprprlemlol  7906  caucvgprprlemopu  7907  caucvgprprlemloc  7911  caucvgprprlemclphr  7913  caucvgprprlemexbt  7914  caucvgprprlem1  7917  caucvgprprlem2  7918  caucvgsr  8010  suplocsrlemb  8014  suplocsrlempr  8015  suplocsrlem  8016  suplocsr  8017  elrealeu  8037  pitonn  8056  nntopi  8102  axcaucvglemval  8105  axcaucvg  8108  axpre-suploclemres  8109  swrdccatin1  11293  swrdccat3blem  11307  fsum2dlemstep  11982  fprod2dlemstep  12170  imasaddfnlemg  13384  cnmpt21  15002