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

Theorem opeq12d 3804
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 3798 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 642 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   <.cop 3643
This theorem is referenced by:  nfopd  3813  moop2  4261  fliftfuns  5813  dfmpt2  6209  fsplit  6223  fnwelem  6230  seqomlem0  6461  seqomlem1  6462  seqomlem4  6465  qliftfuns  6745  xpassen  6956  xpdom2  6957  xpf1o  7023  xpmapenlem  7028  xpmapen  7029  mapunen  7030  xpwdomg  7299  fseqenlem2  7652  nqereu  8553  addpipq2  8560  addpipq  8561  mulpipq2  8563  mulpipq  8564  1nqenq  8586  mulidnq  8587  ltexnq  8599  prlem934  8657  mulsrpr  8698  mulcnsr  8758  mulresr  8761  axcnre  8786  om2uzrdg  11019  uzrdgsuci  11023  ccatopth  11462  splval  11466  splcl  11467  ruclem1  12509  eucalgval2  12751  qnumdenbi  12815  crt  12846  phimullem  12847  prmreclem3  12965  imasval  13414  imasaddvallem  13431  xpsff1o  13470  catidex  13576  cidval  13579  catcocl  13587  catass  13588  oppccofval  13619  sectfval  13654  subccocl  13719  isfunc  13738  funcco  13745  idfuval  13750  idfucl  13755  cofuval  13756  cofuval2  13761  cofucl  13762  cofuass  13763  cofulid  13764  cofurid  13765  resfval  13766  resfval2  13767  funcres  13770  isnat  13821  nati  13829  fucco  13836  fuccoval  13837  coaval  13900  catcisolem  13938  xpcval  13951  xpcco  13957  xpcco2  13961  xpccatid  13962  xpcid  13963  1stfval  13965  2ndfval  13968  1stfcl  13971  2ndfcl  13972  prfval  13973  prf1  13974  prf2fval  13975  prf2  13976  prfcl  13977  prf1st  13978  prf2nd  13979  1st2ndprf  13980  xpcpropd  13982  evlfval  13991  evlf2  13992  evlfcllem  13995  evlfcl  13996  curfval  13997  curf1  13999  curf1cl  14002  curf2cl  14005  curfcl  14006  curfpropd  14007  uncf1  14010  uncf2  14011  curfuncf  14012  uncfcurf  14013  diagval  14014  curf2ndf  14021  hofval  14026  hof2fval  14029  hofcl  14033  yonval  14035  hofpropd  14041  yonedalem21  14047  yonedalem22  14052  yonedalem3  14054  txcnp  17314  upxp  17317  uptx  17319  hauseqlcld  17340  txlm  17342  txkgen  17346  cnmpt1t  17359  cnmpt2t  17367  txhmeo  17494  pt1hmeo  17497  flfcnp2  17702  cnheiborlem  18452  pi1xfrcnvlem  18554  ovollb2lem  18847  ovollb2  18848  ovolshftlem2  18869  ovolscalem2  18873  ioombl1  18919  ioorf  18928  ioorval  18929  ioorinv2  18930  uniioombllem6  18943  dyadval  18947  opnmbl  18957  mbfimaopnlem  19010  limccnp2  19242  dvdsmulf1o  20434  hhssnvt  21842  hhsssh  21846  opfv  23190  xppreima  23211  erdszelem9  23730  erdszelem10  23731  txpcon  23763  txsconlem  23771  sbcopg  24022  11st22nd  25045  eloi  25086  cbicp  25166  isder  25707  homib  25796  idsubfun  25858  idmor  25946  cmp2morp  25958  cmp2morpcats  25961  cmpmorass  25966  morexcmp  25967  cmpidmor2  25969  cmpidmor3  25970  iscatset  25978  heiborlem6  26540  heiborlem7  26541  heiborlem8  26542  pellexlem3  26916  pellex  26920  matval  27465  aoveq123d  28038  bnj1442  29079  bnj1450  29080  bnj1463  29085  bnj1529  29100  dvhvaddcbv  31279  dvhvaddval  31280  dvhopvadd  31283  dvhvaddcomN  31286  dvhvaddass  31287  dvhvscacbv  31288  dvhvscaval  31289  dvhopvsca  31292  dvhgrp  31297  dvhlveclem  31298  dvh0g  31301  dvhopaddN  31304  dvhopspN  31305  dvhopN  31306  cdlemn4  31388  hdmapffval  32019
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator