Theorem opeq1 4208

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

Step	Hyp	Ref	Expression
1		eleq1 2534	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 704	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 4032	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 4101	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 4109	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3957	. 2 |- ( A = B -> if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) ) = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) ) )
7		dfopif 4205	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4205	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2528	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1374   e. wcel 1762   _Vcvv 3108   (/)c0 3780   ifcif 3934   {csn 4022   {cpr 4024   <.cop 4028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029

This theorem is referenced by:  opeq12  4210  opeq1i  4211  opeq1d  4214  oteq1  4217  breq1  4445  cbvopab1  4512  cbvopab1s  4514  opthg  4717  eqvinop  4726  opelopabsb  4752  opelxp  5023  elvvv  5053  opabid2  5125  opeliunxp2  5134  elsnres  5303  elimasng  5356  dmsnopg  5472  cnvsng  5487  funopg  5613  f1osng  5847  f1oprswap  5848  dmfco  5934  fvelrn  6010  fsng  6053  fprg  6063  fvrnressn  6069  fvsng  6088  funfvima3  6130  oveq1  6284  oprabid  6301  dfoprab2  6320  cbvoprab1  6346  elxp4  6720  elxp5  6721  opabex3d  6754  opabex3  6755  op1stg  6788  op2ndg  6789  el2xptp  6819  dfoprab4f  6834  frxp  6885  tfrlem11  7049  omeu  7226  oeeui  7243  elixpsn  7500  fundmen  7581  xpsnen  7593  xpassen  7603  xpf1o  7671  unxpdomlem1  7716  dfac5lem1  8495  dfac5lem4  8498  axdc4lem  8826  nqereu  9298  mulcanenq  9329  archnq  9349  prlem934  9402  supsrlem  9479  supsr  9480  swrdccatin1  12660  swrdccat3blem  12672  fsum2dlem  13536  vdwlem10  14358  imasaddfnlem  14774  catideu  14921  iscatd2  14927  catlid  14929  catpropd  14956  symg2bas  16213  efgmval  16521  efgi  16528  vrgpval  16576  gsumcom2  16789  txkgen  19883  cnmpt21  19902  xkoinjcn  19918  txcon  19920  pt1hmeo  20037  cnextfvval  20295  divstgplem  20349  dvbsss  22036  axlowdim2  23934  axlowdim  23935  axcontlem10  23947  axcontlem12  23949  0eusgraiff0rgra  24603  drngoi  25073  isdivrngo  25097  isnvlem  25167  br8d  27124  cnvoprab  27206  prsrn  27521  eulerpartlemgvv  27943  fprod2dlem  28675  br8  28750  br6  28751  br4  28752  eldm3  28756  dfdm5  28771  elfuns  29130  brimg  29152  brapply  29153  brrestrict  29164  dfrdg4  29165  cgrdegen  29219  brofs  29220  cgrextend  29223  brifs  29258  ifscgr  29259  brcgr3  29261  brcolinear2  29273  colineardim1  29276  brfs  29294  idinside  29299  btwnconn1lem7  29308  btwnconn1lem11  29312  btwnconn1lem12  29313  brsegle  29323  outsideofeu  29346  fvray  29356  linedegen  29358  fvline  29359  dropab1  30891  relopabVD  32658  bj-inftyexpiinv  33560  bj-inftyexpidisj  33562  dicelval3  35854  dihjatcclem4  36095