Theorem opeq1 4047

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 2493	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 697	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3875	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 3942	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3950	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3800	. 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 4044	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4044	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2490	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   _Vcvv 2962   (/)c0 3625   ifcif 3779   {csn 3865   {cpr 3867   <.cop 3871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872

This theorem is referenced by:  opeq12  4049  opeq1i  4050  opeq1d  4053  oteq1  4056  breq1  4283  cbvopab1  4350  cbvopab1s  4352  opthg  4555  eqvinop  4563  opelopabsb  4588  opelxp  4856  elvvv  4885  opabid2  4956  opeliunxp2  4965  elsnres  5134  elimasng  5183  dmsnopg  5298  cnvsng  5313  funopg  5438  f1osng  5667  f1oprswap  5668  dmfco  5753  fvelrn  5827  fsng  5869  fprg  5878  fvsng  5899  funfvima3  5941  oveq1  6087  oprabid  6104  dfoprab2  6122  cbvoprab1  6147  elxp4  6511  elxp5  6512  opabex3d  6544  opabex3  6545  op1stg  6578  op2ndg  6579  dfoprab4f  6621  frxp  6671  tfrlem11  6833  omeu  7012  oeeui  7029  elixpsn  7290  fundmen  7371  xpsnen  7383  xpassen  7393  xpf1o  7461  unxpdomlem1  7505  dfac5lem1  8281  dfac5lem4  8284  axdc4lem  8612  nqereu  9085  mulcanenq  9116  archnq  9136  prlem934  9189  supsrlem  9265  supsr  9266  swrdccatin1  12357  swrdccat3blem  12369  fsum2dlem  13220  vdwlem10  14033  imasaddfnlem  14448  catideu  14595  iscatd2  14601  catlid  14603  catpropd  14630  symg2bas  15882  efgmval  16188  efgi  16195  vrgpval  16243  gsumcom2  16440  txkgen  19066  cnmpt21  19085  xkoinjcn  19101  txcon  19103  pt1hmeo  19220  cnextfvval  19478  divstgplem  19532  dvbsss  21218  axlowdim2  23028  axlowdim  23029  axcontlem10  23041  axcontlem12  23043  drngoi  23716  isdivrngo  23740  isnvlem  23810  br8d  25765  cnvoprab  25846  prsrn  26198  eulerpartlemgvv  26606  fprod2dlem  27337  br8  27412  br6  27413  br4  27414  eldm3  27418  dfdm5  27433  elfuns  27792  brimg  27814  brapply  27815  brrestrict  27826  dfrdg4  27827  cgrdegen  27881  brofs  27882  cgrextend  27885  brifs  27920  ifscgr  27921  brcgr3  27923  brcolinear2  27935  colineardim1  27938  brfs  27956  idinside  27961  btwnconn1lem7  27970  btwnconn1lem11  27974  btwnconn1lem12  27975  brsegle  27985  outsideofeu  28008  fvray  28018  linedegen  28020  fvline  28021  dropab1  29545  el2xptp  29969  fvelrnfvelrnressn  29994  0eusgraiff0rgra  30395  relopabVD  31336  bj-inftyexpiinv  32108  bj-inftyexpidisj  32110  dicelval3  34395  dihjatcclem4  34636