Theorem opeq1 4161

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 2476	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 705	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3984	. . . 4 |- ( A = B -> { A } = { B } )
4		preq1 4053	. . . 4 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 4061	. . 3 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	2, 5	ifbieq1d 3910	. 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 4158	. 2 |- <. A , C >. = if ( ( A e. _V /\ C e. _V ) , { { A } , { A , C } } , (/) )
8		dfopif 4158	. 2 |- <. B , C >. = if ( ( B e. _V /\ C e. _V ) , { { B } , { B , C } } , (/) )
9	6, 7, 8	3eqtr4g 2470	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1407   e. wcel 1844   _Vcvv 3061   (/)c0 3740   ifcif 3887   {csn 3974   {cpr 3976   <.cop 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981

This theorem is referenced by:  opeq12  4163  opeq1i  4164  opeq1d  4167  oteq1  4170  breq1  4400  cbvopab1  4467  cbvopab1s  4469  opthg  4668  eqvinop  4677  opelopabsb  4702  opelxp  4855  elvvv  4885  opabid2  4955  opeliunxp2  4964  elsnres  5132  elimasng  5185  dmsnopg  5297  cnvsng  5312  funopg  5603  f1osng  5839  f1oprswap  5840  dmfco  5925  fvelrn  6004  fsng  6052  fprg  6062  fvrnressn  6068  fvsng  6087  funfvima3  6132  oveq1  6287  oprabid  6307  dfoprab2  6326  cbvoprab1  6352  elxp4  6730  elxp5  6731  opabex3d  6764  opabex3  6765  op1stg  6798  op2ndg  6799  el2xptp  6829  dfoprab4f  6844  frxp  6896  tfrlem11  7093  omeu  7273  oeeui  7290  elixpsn  7548  fundmen  7629  xpsnen  7641  xpassen  7651  xpf1o  7719  unxpdomlem1  7761  dfac5lem1  8538  dfac5lem4  8541  axdc4lem  8869  nqereu  9339  mulcanenq  9370  archnq  9390  prlem934  9443  supsrlem  9520  supsr  9521  swrdccatin1  12766  swrdccat3blem  12778  fsum2dlem  13738  fprod2dlem  13938  vdwlem10  14719  imasaddfnlem  15144  catideu  15291  iscatd2  15297  catlid  15299  catpropd  15324  symg2bas  16749  efgmval  17056  efgi  17063  vrgpval  17111  gsumcom2  17326  txkgen  20447  cnmpt21  20466  xkoinjcn  20482  txcon  20484  pt1hmeo  20601  cnextfvval  20859  qustgplem  20913  dvbsss  22600  axlowdim2  24692  axlowdim  24693  axcontlem10  24705  axcontlem12  24707  0eusgraiff0rgra  25368  drngoi  25836  isdivrngo  25860  isnvlem  25930  br8d  27913  elsnxp  27919  cnvoprab  28006  prsrn  28363  esum2dlem  28552  eulerpartlemgvv  28834  br8  29982  br6  29983  br4  29984  eldm3  29988  br1steqg  30002  br2ndeqg  30003  dfdm5  30004  elfuns  30266  brimg  30288  brapply  30289  brsuccf  30292  brrestrict  30300  dfrdg4  30302  cgrdegen  30355  brofs  30356  cgrextend  30359  brifs  30394  ifscgr  30395  brcgr3  30397  brcolinear2  30409  colineardim1  30412  brfs  30430  idinside  30435  btwnconn1lem7  30444  btwnconn1lem11  30448  btwnconn1lem12  30449  brsegle  30459  outsideofeu  30482  fvray  30492  linedegen  30494  fvline  30495  bj-inftyexpiinv  31188  bj-inftyexpidisj  31190  dicelval3  34213  dihjatcclem4  34454  dropab1  36217  relopabVD  36745