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

Theorem opeq12d 4016
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 4010 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 644 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   <.cop 3841
This theorem is referenced by:  nfopd  4025  moop2  4480  fliftfuns  6065  dfmpt2  6466  fsplit  6480  fnwelem  6490  seqomlem0  6735  seqomlem1  6736  seqomlem4  6739  qliftfuns  7020  xpassen  7231  xpdom2  7232  xpf1o  7298  xpmapenlem  7303  xpmapen  7304  mapunen  7305  xpwdomg  7582  fseqenlem2  7937  nqereu  8837  addpipq2  8844  addpipq  8845  mulpipq2  8847  mulpipq  8848  1nqenq  8870  mulidnq  8871  ltexnq  8883  prlem934  8941  mulsrpr  8982  mulcnsr  9042  mulresr  9045  axcnre  9070  om2uzrdg  11327  uzrdgsuci  11331  ccatopth  11807  splval  11811  splcl  11812  ruclem1  12861  eucalgval2  13103  qnumdenbi  13167  crt  13198  phimullem  13199  prmreclem3  13317  imasval  13768  imasaddvallem  13785  xpsff1o  13824  catidex  13930  cidval  13933  catcocl  13941  catass  13942  oppccofval  13973  sectfval  14008  subccocl  14073  isfunc  14092  funcco  14099  idfuval  14104  idfucl  14109  cofuval  14110  cofuval2  14115  cofucl  14116  cofuass  14117  cofulid  14118  cofurid  14119  resfval  14120  resfval2  14121  funcres  14124  isnat  14175  nati  14183  fucco  14190  fuccoval  14191  coaval  14254  catcisolem  14292  xpcval  14305  xpcco  14311  xpcco2  14315  xpccatid  14316  xpcid  14317  1stfval  14319  2ndfval  14322  1stfcl  14325  2ndfcl  14326  prfval  14327  prf1  14328  prf2fval  14329  prf2  14330  prfcl  14331  prf1st  14332  prf2nd  14333  1st2ndprf  14334  xpcpropd  14336  evlfval  14345  evlf2  14346  evlfcllem  14349  evlfcl  14350  curfval  14351  curf1  14353  curf1cl  14356  curf2cl  14359  curfcl  14360  curfpropd  14361  uncf1  14364  uncf2  14365  curfuncf  14366  uncfcurf  14367  diagval  14368  curf2ndf  14375  hofval  14380  hof2fval  14383  hofcl  14387  yonval  14389  hofpropd  14395  yonedalem21  14401  yonedalem22  14406  yonedalem3  14408  txcnp  17683  upxp  17686  uptx  17688  hauseqlcld  17709  txlm  17711  txkgen  17715  cnmpt1t  17728  cnmpt2t  17736  txhmeo  17866  pt1hmeo  17869  flfcnp2  18070  ucnimalem  18341  ucnima  18342  fmucndlem  18352  fmucnd  18353  cnheiborlem  19010  pi1xfrcnvlem  19112  ovollb2lem  19415  ovollb2  19416  ovolshftlem2  19437  ovolscalem2  19441  ioombl1  19487  ioorf  19496  ioorval  19497  ioorinv2  19498  uniioombllem6  19511  dyadval  19515  opnmbl  19525  mbfimaopnlem  19576  limccnp2  19810  dvdsmulf1o  21010  hhssnvt  22796  hhsssh  22800  opfv  24089  xppreima  24090  ofpreima  24112  qqhval2  24397  rrvadd  24741  erdszelem9  24916  erdszelem10  24917  txpcon  24950  txsconlem  24958  sbcopg  25157  opnmbllem0  26278  mblfinlem1  26279  mblfinlem2  26280  heiborlem6  26563  heiborlem7  26564  heiborlem8  26565  pellexlem3  26932  pellex  26936  aoveq123d  28056  swrdswrd0  28259  swrdccatin2d  28279  cshfn  28292  2cshw1lem1  28306  2cshw2lem1  28310  bnj1442  29516  bnj1450  29517  bnj1463  29522  bnj1529  29537  dvhvaddcbv  31985  dvhvaddval  31986  dvhopvadd  31989  dvhvaddcomN  31992  dvhvaddass  31993  dvhvscacbv  31994  dvhvscaval  31995  dvhopvsca  31998  dvhgrp  32003  dvhlveclem  32004  dvh0g  32007  dvhopaddN  32010  dvhopspN  32011  dvhopN  32012  cdlemn4  32094  hdmapffval  32725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847
  Copyright terms: Public domain W3C validator