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

Theorem opeq12d 4064
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 4058 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 656 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364   <.cop 3880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881
This theorem is referenced by:  nfopd  4073  csbopg  4074  moop2  4583  fnprb  5933  fliftfuns  6004  dfmpt2  6662  fsplit  6676  fnwelem  6686  seqomlem0  6900  seqomlem1  6901  seqomlem4  6904  qliftfuns  7183  xpassen  7401  xpdom2  7402  xpf1o  7469  xpmapenlem  7474  xpmapen  7475  mapunen  7476  xpwdomg  7796  fseqenlem2  8191  nqereu  9094  addpipq2  9101  addpipq  9102  mulpipq2  9104  mulpipq  9105  1nqenq  9127  mulidnq  9128  ltexnq  9140  prlem934  9198  mulsrpr  9239  mulcnsr  9299  mulresr  9302  axcnre  9327  om2uzrdg  11775  uzrdgsuci  11779  2swrd1eqwrdeq  12344  swrdswrd0  12352  ccatopth  12360  swrdccatin2d  12387  splval  12389  splcl  12390  cshfn  12423  repswcshw  12442  2swrd2eqwrdeq  12549  ruclem1  13509  eucalgval2  13752  qnumdenbi  13818  crt  13849  phimullem  13850  prmreclem3  13975  imasval  14445  imasaddvallem  14463  xpsff1o  14502  catidex  14608  cidval  14611  catcocl  14619  catass  14620  oppccofval  14651  sectfval  14686  subccocl  14751  isfunc  14770  funcco  14777  idfuval  14782  idfucl  14787  cofuval  14788  cofuval2  14793  cofucl  14794  cofuass  14795  cofulid  14796  cofurid  14797  resfval  14798  resfval2  14799  funcres  14802  isnat  14853  nati  14861  fucco  14868  fuccoval  14869  coaval  14932  catcisolem  14970  xpcval  14983  xpcco  14989  xpcco2  14993  xpccatid  14994  xpcid  14995  1stfval  14997  2ndfval  15000  1stfcl  15003  2ndfcl  15004  prfval  15005  prf1  15006  prf2fval  15007  prf2  15008  prfcl  15009  prf1st  15010  prf2nd  15011  1st2ndprf  15012  xpcpropd  15014  evlfval  15023  evlf2  15024  evlfcllem  15027  evlfcl  15028  curfval  15029  curf1  15031  curf1cl  15034  curf2cl  15037  curfcl  15038  curfpropd  15039  uncf1  15042  uncf2  15043  curfuncf  15044  uncfcurf  15045  diagval  15046  curf2ndf  15053  hofval  15058  hof2fval  15061  hofcl  15065  yonval  15067  hofpropd  15073  yonedalem21  15079  yonedalem22  15084  yonedalem3  15086  symg2bas  15896  txcnp  19152  upxp  19155  uptx  19157  hauseqlcld  19178  txlm  19180  txkgen  19184  cnmpt1t  19197  cnmpt2t  19205  txhmeo  19335  pt1hmeo  19338  flfcnp2  19539  ucnimalem  19814  ucnima  19815  fmucndlem  19825  fmucnd  19826  cnheiborlem  20485  pi1xfrcnvlem  20587  ovollb2lem  20930  ovollb2  20931  ovolshftlem2  20952  ovolscalem2  20956  ioombl1  21002  ioorf  21012  ioorval  21013  ioorinv2  21014  uniioombllem6  21027  dyadval  21031  opnmbl  21041  mbfimaopnlem  21092  limccnp2  21326  dvdsmulf1o  22493  ebtwntg  23163  hhssnvt  24601  hhsssh  24605  opfv  25898  xppreima  25899  ofpreima  25919  fgreu  25925  qqhval2  26347  rrvadd  26765  erdszelem9  27017  erdszelem10  27018  txpcon  27051  txsconlem  27059  opnmbllem0  28352  mblfinlem1  28353  mblfinlem2  28354  heiborlem6  28640  heiborlem7  28641  heiborlem8  28642  pellexlem3  29097  pellex  29101  aoveq123d  30009  numclwlk1lem2fv  30611  numclwlk1lem2fo  30613  mat1dimmul  30755  bnj1442  31874  bnj1450  31875  bnj1463  31880  bnj1529  31895  dvhvaddcbv  34456  dvhvaddval  34457  dvhopvadd  34460  dvhvaddcomN  34463  dvhvaddass  34464  dvhvscacbv  34465  dvhvscaval  34466  dvhopvsca  34469  dvhgrp  34474  dvhlveclem  34475  dvh0g  34478  dvhopaddN  34481  dvhopspN  34482  dvhopN  34483  cdlemn4  34565  hdmapffval  35196
  Copyright terms: Public domain W3C validator