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

Theorem opeq2 4159
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 2474 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 702 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 4051 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 4057 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3907 . 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 4155 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4155 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2468 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   _Vcvv 3058   (/)c0 3737   ifcif 3884   {csn 3971   {cpr 3973   <.cop 3977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978
This theorem is referenced by:  opeq12  4160  opeq2i  4162  opeq2d  4165  oteq2  4168  oteq3  4169  breq2  4398  cbvopab2  4465  cbvopab2v  4468  opthg  4665  eqvinop  4674  opelopabsb  4699  dfid3  4738  opelxp  4852  opabid2  4952  elrn2g  5013  opeldm  5026  elrn2  5062  opelresg  5100  iss  5140  elimasng  5182  issref  5200  dmsnopg  5294  cnvsng  5309  funopg  5600  f1osng  5836  f1oprswap  5837  tz6.12f  5866  fvn0ssdmfun  5999  fsn  6047  fsng  6049  fprg  6059  fvsng  6084  oveq2  6285  cbvoprab2  6350  ovg  6421  elxp4  6727  elxp5  6728  opabex3d  6761  opabex3  6762  op1stg  6795  op2ndg  6796  op1steq  6825  dfoprab4f  6841  seqomlem2  7152  omeu  7270  oeeui  7287  ralxpmap  7505  elixpsn  7545  ixpsnf1o  7546  mapsnen  7630  xpsnen  7638  xpassen  7648  xpf1o  7716  unxpdomlem1  7758  axdc4lem  8866  nqereu  9336  mulcanenq  9367  elreal  9537  ax1rid  9567  fseq1p1m1  11805  swrdccatin1  12762  swrdccat3blem  12774  swrdccatid  12776  swrdccatin12d  12780  wrdlen2  12940  ruclem1  14171  imasaddfnlem  15140  imasvscafn  15149  catidex  15286  catpropd  15320  funcsetcestrclem1  15745  symg2bas  16745  psgnunilem5  16841  efgi  17059  gsumcom2  17322  mat1rhmval  19271  mat1ric  19279  txkgen  20443  cnmpt21  20462  xkoinjcn  20478  txcon  20480  xpstopnlem1  20600  qustgplem  20909  metustidOLD  21352  metustid  21353  axlowdim2  24667  axlowdim  24668  axcontlem2  24672  axcontlem3  24673  axcontlem4  24674  axcontlem9  24679  axcontlem10  24680  axcontlem11  24681  1pthoncl  24998  2pthoncl  25009  wwlknextbi  25129  wwlkextinj  25134  wwlkextsur  25135  clwwlkfo  25201  0eusgraiff0rgra  25343  drngoi  25809  isdivrngo  25833  vcoprne  25872  isnvlem  25903  br8d  27886  prsdm  28335  eulerpartlemgvv  28807  bnj941  29145  bnj944  29310  cvmlift2lem1  29586  cvmlift2lem12  29598  br8  29956  br6  29957  br4  29958  fprb  29973  br1steqg  29976  br2ndeqg  29977  dfrn5  29979  elima4  29981  pprodss4v  30209  brimg  30262  brapply  30263  brsuccf  30266  brrestrict  30274  dfrdg4  30276  cgrtriv  30327  brofs  30330  segconeu  30336  btwntriv2  30337  transportprops  30359  brifs  30368  ifscgr  30369  brcgr3  30371  cgrxfr  30380  brcolinear2  30383  colineardim1  30386  brfs  30404  idinside  30409  btwnconn1lem7  30418  btwnconn1lem11  30422  btwnconn1lem12  30423  btwnconn1lem14  30425  brsegle  30433  seglerflx  30437  seglemin  30438  segleantisym  30440  btwnsegle  30442  outsideofeu  30456  outsidele  30457  linedegen  30468  fvline  30469  dibelval3  34147  diblsmopel  34171  dihjatcclem4  34421  dfhe3  35735  dffrege115  35939  dropab2  36185  relopabVD  36712  pfxval  37851
  Copyright terms: Public domain W3C validator