Theorem opeq2 4403

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

Assertion

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

Proof of Theorem opeq2

Step	Hyp	Ref	Expression
1		eleq1 2689	. . . 4 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 740	. . 3 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		preq2 4269	. . . 4 |- ( A = B -> { C , A } = { C , B } )
4	3	preq2d 4275	. . 3 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
5	2, 4	ifbieq1d 4109	. 2 |- ( A = B -> if ( ( C e. _V /\ A e. _V ) , { { C } , { C , A } } , (/) ) = if ( ( C e. _V /\ B e. _V ) , { { C } , { C , B } } , (/) ) )
6		dfopif 4399	. 2 |- <. C , A >. = if ( ( C e. _V /\ A e. _V ) , { { C } , { C , A } } , (/) )
7		dfopif 4399	. 2 |- <. C , B >. = if ( ( C e. _V /\ B e. _V ) , { { C } , { C , B } } , (/) )
8	5, 6, 7	3eqtr4g 2681	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200   (/)c0 3915   ifcif 4086   {csn 4177   {cpr 4179   <.cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  opeq12  4404  opeq2i  4406  opeq2d  4409  oteq2  4412  oteq3  4413  breq2  4657  cbvopab2  4724  cbvopab2v  4727  opthg  4946  eqvinop  4955  opelopabsb  4985  dfid3  5025  opelxp  5146  relopabi  5245  opabid2  5251  elrn2g  5313  opeldmd  5327  opeldm  5328  elrn2  5365  opelresg  5404  iss  5447  elimasng  5491  issref  5509  dmsnopg  5606  cnvsng  5621  funopg  5922  f1osng  6177  f1oprswap  6180  tz6.12f  6212  fvn0ssdmfun  6350  fsn  6402  fsng  6404  funsneqopsn  6417  fprg  6422  fvsng  6447  oveq2  6658  cbvoprab2  6728  ovg  6799  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  op1stg  7180  op2ndg  7181  op1steq  7210  dfoprab4f  7226  seqomlem2  7546  omeu  7665  oeeui  7682  ralxpmap  7907  elixpsn  7947  ixpsnf1o  7948  mapsnen  8035  xpsnen  8044  xpassen  8054  xpf1o  8122  unxpdomlem1  8164  axdc4lem  9277  nqereu  9751  mulcanenq  9782  elreal  9952  ax1rid  9982  fseq1p1m1  12414  swrdccatin1  13483  swrdccat3blem  13495  swrdccatid  13497  swrdccatin12d  13501  wrdlen2  13688  ruclem1  14960  imasaddfnlem  16188  imasvscafn  16197  catidex  16335  catpropd  16369  funcsetcestrclem1  16794  symg2bas  17818  psgnunilem5  17914  efgi  18132  gsumcom2  18374  mat1rhmval  20285  mat1ric  20293  txkgen  21455  cnmpt21  21474  xkoinjcn  21490  txconn  21492  xpstopnlem1  21612  qustgplem  21924  metustid  22359  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem3  25846  axcontlem4  25847  axcontlem9  25852  axcontlem10  25853  axcontlem11  25854  cusgrexg  26340  rgrusgrprc  26485  wwlksnextbi  26789  wwlksnextinj  26794  wwlksnextsur  26795  clwwlksfo  26918  clwlksfclwwlk  26962  isnvlem  27465  br8d  29422  prsdm  29960  eulerpartlemgvv  30438  reprsuc  30693  bnj941  30843  bnj944  31008  cvmlift2lem1  31284  cvmlift2lem12  31296  br8  31646  br6  31647  br4  31648  fprb  31669  br1steqgOLD  31674  br2ndeqgOLD  31675  dfrn5  31677  elima4  31679  pprodss4v  31991  brimg  32044  brapply  32045  brsuccf  32048  brrestrict  32056  dfrdg4  32058  cgrtriv  32109  brofs  32112  segconeu  32118  btwntriv2  32119  transportprops  32141  brifs  32150  ifscgr  32151  brcgr3  32153  cgrxfr  32162  brcolinear2  32165  colineardim1  32168  brfs  32186  idinside  32191  btwnconn1lem7  32200  btwnconn1lem11  32204  btwnconn1lem12  32205  btwnconn1lem14  32207  brsegle  32215  seglerflx  32219  seglemin  32220  segleantisym  32222  btwnsegle  32224  outsideofeu  32238  outsidele  32239  linedegen  32250  fvline  32251  finxpreclem6  33233  finxpsuclem  33234  curfv  33389  poimirlem4  33413  poimirlem26  33435  isdivrngo  33749  drngoi  33750  iss2  34112  dibelval3  36436  diblsmopel  36460  dihjatcclem4  36710  dfhe3  38069  dffrege115  38272  dropab2  38652  relopabVD  39137  projf1o  39386  mapsnend  39391  sge0xp  40646  hoidmv1le  40808  pfxval  41383