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

Theorem opeq12d 4152
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Hypotheses
Ref Expression
opeq1d.1  |-  ( ph  ->  A  =  B )
opeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
opeq12d  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )

Proof of Theorem opeq12d
StepHypRef Expression
1 opeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opeq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 opeq12 4146 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 659 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   <.cop 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-rab 2751  df-v 3049  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-sn 3958  df-pr 3960  df-op 3964
This theorem is referenced by:  nfopd  4161  csbopg  4162  moop2  4669  fsn2g  5987  fnprb  6046  fnpr2g  6047  fliftfuns  6131  dfmpt2  6807  fsplit  6822  fnwelem  6832  seqomlem0  7050  seqomlem1  7051  seqomlem4  7054  qliftfuns  7334  xpassen  7548  xpdom2  7549  xpf1o  7616  xpmapenlem  7621  xpmapen  7622  mapunen  7623  xpwdomg  7944  fseqenlem2  8337  nqereu  9236  addpipq2  9243  addpipq  9244  mulpipq2  9246  mulpipq  9247  1nqenq  9269  mulidnq  9270  ltexnq  9282  prlem934  9340  addsrmo  9379  mulsrmo  9380  addsrpr  9381  mulsrpr  9382  mulcnsr  9442  mulresr  9445  axcnre  9470  om2uzrdg  11989  uzrdgsuci  11993  2swrd1eqwrdeq  12609  swrdswrd0  12617  ccatopth  12625  swrdccatin2d  12655  splval  12657  splcl  12658  cshfn  12691  repswcshw  12710  2swrd2eqwrdeq  12821  ruclem1  13985  eucalgval2  14231  qnumdenbi  14298  crt  14329  phimullem  14330  prmreclem3  14457  ressval3d  14717  imasval  14937  imasaddvallem  14955  xpsff1o  14994  catidex  15100  cidval  15103  catcocl  15111  catass  15112  oppccofval  15141  sectfval  15176  subccocl  15270  isfunc  15289  funcco  15296  idfuval  15301  idfucl  15306  cofuval  15307  cofuval2  15312  cofucl  15313  cofuass  15314  cofulid  15315  cofurid  15316  resfval  15317  resfval2  15318  funcres  15321  isnat  15372  nati  15380  fucco  15387  fuccoval  15388  coaval  15483  catcisolem  15521  xpcval  15582  xpcco  15588  xpcco2  15592  xpccatid  15593  xpcid  15594  1stfval  15596  2ndfval  15599  1stfcl  15602  2ndfcl  15603  prfval  15604  prf1  15605  prf2fval  15606  prf2  15607  prfcl  15608  prf1st  15609  prf2nd  15610  1st2ndprf  15611  xpcpropd  15613  evlfval  15622  evlf2  15623  evlfcllem  15626  evlfcl  15627  curfval  15628  curf1  15630  curf1cl  15633  curf2cl  15636  curfcl  15637  curfpropd  15638  uncf1  15641  uncf2  15642  curfuncf  15643  uncfcurf  15644  diagval  15645  curf2ndf  15652  hofval  15657  hof2fval  15660  hofcl  15664  yonval  15666  hofpropd  15672  yonedalem21  15678  yonedalem22  15683  yonedalem3  15685  symg2bas  16559  mat1dimmul  19082  txcnp  20225  upxp  20228  uptx  20230  hauseqlcld  20251  txlm  20253  txkgen  20257  cnmpt1t  20270  cnmpt2t  20278  txhmeo  20408  pt1hmeo  20411  flfcnp2  20612  ucnimalem  20887  ucnima  20888  fmucndlem  20898  fmucnd  20899  cnheiborlem  21558  pi1xfrcnvlem  21660  ovollb2lem  22003  ovollb2  22004  ovolshftlem2  22025  ovolscalem2  22029  ioombl1  22076  ioorf  22086  ioorval  22087  ioorinv2  22088  uniioombllem6  22101  dyadval  22105  opnmbl  22115  mbfimaopnlem  22166  limccnp2  22400  dvdsmulf1o  23606  ebtwntg  24427  usgrac  24493  numclwlk1lem2fv  25235  numclwlk1lem2fo  25237  hhssnvt  26319  hhsssh  26323  opfv  27656  xppreima  27657  aciunf1lem  27678  ofpreima  27683  fgreu  27689  fimaproj  28021  qtophaus  28024  qqhval2  28147  esum2dlem  28271  rrvadd  28610  erdszelem9  28868  erdszelem10  28869  txpcon  28902  txsconlem  28910  msubval  29110  msubco  29116  mvhval  29119  msubvrs  29145  opnmbllem0  30251  mblfinlem1  30252  mblfinlem2  30253  heiborlem6  30514  heiborlem7  30515  heiborlem8  30516  pellexlem3  30968  pellex  30972  dvnprodlem1  31944  dvnprodlem3  31946  etransclem44  32262  aoveq123d  32464  pfxsuff1eqwrdeq  32617  inclfusubc  32908  funcrngcsetc  33041  funcrngcsetcALT  33042  funcringcsetc  33078  bnj1442  34487  bnj1450  34488  bnj1463  34493  bnj1529  34508  dvhvaddcbv  37264  dvhvaddval  37265  dvhopvadd  37268  dvhvaddcomN  37271  dvhvaddass  37272  dvhvscacbv  37273  dvhvscaval  37274  dvhopvsca  37277  dvhgrp  37282  dvhlveclem  37283  dvh0g  37286  dvhopaddN  37289  dvhopspN  37290  dvhopN  37291  cdlemn4  37373  hdmapffval  38004
  Copyright terms: Public domain W3C validator