MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq2 Structured version   Unicode version

Theorem opeq2 4186
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
StepHypRef Expression
1 eleq1 2495 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 709 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 4078 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 4084 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3933 . 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 4182 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4182 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2489 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   _Vcvv 3082   (/)c0 3762   ifcif 3910   {csn 3997   {cpr 3999   <.cop 4003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004
This theorem is referenced by:  opeq12  4187  opeq2i  4189  opeq2d  4192  oteq2  4195  oteq3  4196  breq2  4425  cbvopab2  4493  cbvopab2v  4496  opthg  4694  eqvinop  4703  opelopabsb  4728  dfid3  4767  opelxp  4881  opabid2  4981  elrn2g  5042  opeldm  5055  elrn2  5091  opelresg  5129  iss  5169  elimasng  5211  issref  5230  dmsnopg  5324  cnvsng  5339  funopg  5631  f1osng  5867  f1oprswap  5868  tz6.12f  5897  fvn0ssdmfun  6026  fsn  6074  fsng  6076  fprg  6086  fvsng  6111  oveq2  6311  cbvoprab2  6376  ovg  6447  elxp4  6749  elxp5  6750  opabex3d  6783  opabex3  6784  op1stg  6817  op2ndg  6818  op1steq  6847  dfoprab4f  6863  seqomlem2  7174  omeu  7292  oeeui  7309  ralxpmap  7527  elixpsn  7567  ixpsnf1o  7568  mapsnen  7652  xpsnen  7660  xpassen  7670  xpf1o  7738  unxpdomlem1  7780  axdc4lem  8887  nqereu  9356  mulcanenq  9387  elreal  9557  ax1rid  9587  fseq1p1m1  11870  swrdccatin1  12835  swrdccat3blem  12847  swrdccatid  12849  swrdccatin12d  12853  wrdlen2  13017  ruclem1  14276  imasaddfnlem  15427  imasvscafn  15436  catidex  15573  catpropd  15607  funcsetcestrclem1  16032  symg2bas  17032  psgnunilem5  17128  efgi  17362  gsumcom2  17600  mat1rhmval  19496  mat1ric  19504  txkgen  20659  cnmpt21  20678  xkoinjcn  20694  txcon  20696  xpstopnlem1  20816  qustgplem  21127  metustid  21561  axlowdim2  24982  axlowdim  24983  axcontlem2  24987  axcontlem3  24988  axcontlem4  24989  axcontlem9  24994  axcontlem10  24995  axcontlem11  24996  1pthoncl  25314  2pthoncl  25325  wwlknextbi  25445  wwlkextinj  25450  wwlkextsur  25451  clwwlkfo  25517  0eusgraiff0rgra  25659  drngoi  26127  isdivrngo  26151  vcoprne  26190  isnvlem  26221  br8d  28214  prsdm  28722  eulerpartlemgvv  29211  bnj941  29586  bnj944  29751  cvmlift2lem1  30027  cvmlift2lem12  30039  br8  30397  br6  30398  br4  30399  fprb  30414  br1steqg  30417  br2ndeqg  30418  dfrn5  30420  elima4  30422  pprodss4v  30650  brimg  30703  brapply  30704  brsuccf  30707  brrestrict  30715  dfrdg4  30717  cgrtriv  30768  brofs  30771  segconeu  30777  btwntriv2  30778  transportprops  30800  brifs  30809  ifscgr  30810  brcgr3  30812  cgrxfr  30821  brcolinear2  30824  colineardim1  30827  brfs  30845  idinside  30850  btwnconn1lem7  30859  btwnconn1lem11  30863  btwnconn1lem12  30864  btwnconn1lem14  30866  brsegle  30874  seglerflx  30878  seglemin  30879  segleantisym  30881  btwnsegle  30883  outsideofeu  30897  outsidele  30898  linedegen  30909  fvline  30910  finxpreclem6  31746  finxpsuclem  31747  poimirlem4  31902  poimirlem26  31924  dibelval3  34678  diblsmopel  34702  dihjatcclem4  34952  dfhe3  36272  dffrege115  36476  dropab2  36703  relopabVD  37203  projf1o  37368  sge0xp  38103  pfxval  38680  funsneqopsn  38765
  Copyright terms: Public domain W3C validator