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

Theorem opeq12d 3984
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 3978 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 643 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   <.cop 3809
This theorem is referenced by:  nfopd  3993  moop2  4443  fliftfuns  6027  dfmpt2  6428  fsplit  6442  fnwelem  6452  seqomlem0  6697  seqomlem1  6698  seqomlem4  6701  qliftfuns  6982  xpassen  7193  xpdom2  7194  xpf1o  7260  xpmapenlem  7265  xpmapen  7266  mapunen  7267  xpwdomg  7542  fseqenlem2  7895  nqereu  8795  addpipq2  8802  addpipq  8803  mulpipq2  8805  mulpipq  8806  1nqenq  8828  mulidnq  8829  ltexnq  8841  prlem934  8899  mulsrpr  8940  mulcnsr  9000  mulresr  9003  axcnre  9028  om2uzrdg  11284  uzrdgsuci  11288  ccatopth  11764  splval  11768  splcl  11769  ruclem1  12818  eucalgval2  13060  qnumdenbi  13124  crt  13155  phimullem  13156  prmreclem3  13274  imasval  13725  imasaddvallem  13742  xpsff1o  13781  catidex  13887  cidval  13890  catcocl  13898  catass  13899  oppccofval  13930  sectfval  13965  subccocl  14030  isfunc  14049  funcco  14056  idfuval  14061  idfucl  14066  cofuval  14067  cofuval2  14072  cofucl  14073  cofuass  14074  cofulid  14075  cofurid  14076  resfval  14077  resfval2  14078  funcres  14081  isnat  14132  nati  14140  fucco  14147  fuccoval  14148  coaval  14211  catcisolem  14249  xpcval  14262  xpcco  14268  xpcco2  14272  xpccatid  14273  xpcid  14274  1stfval  14276  2ndfval  14279  1stfcl  14282  2ndfcl  14283  prfval  14284  prf1  14285  prf2fval  14286  prf2  14287  prfcl  14288  prf1st  14289  prf2nd  14290  1st2ndprf  14291  xpcpropd  14293  evlfval  14302  evlf2  14303  evlfcllem  14306  evlfcl  14307  curfval  14308  curf1  14310  curf1cl  14313  curf2cl  14316  curfcl  14317  curfpropd  14318  uncf1  14321  uncf2  14322  curfuncf  14323  uncfcurf  14324  diagval  14325  curf2ndf  14332  hofval  14337  hof2fval  14340  hofcl  14344  yonval  14346  hofpropd  14352  yonedalem21  14358  yonedalem22  14363  yonedalem3  14365  txcnp  17640  upxp  17643  uptx  17645  hauseqlcld  17666  txlm  17668  txkgen  17672  cnmpt1t  17685  cnmpt2t  17693  txhmeo  17823  pt1hmeo  17826  flfcnp2  18027  ucnimalem  18298  ucnima  18299  fmucndlem  18309  fmucnd  18310  cnheiborlem  18967  pi1xfrcnvlem  19069  ovollb2lem  19372  ovollb2  19373  ovolshftlem2  19394  ovolscalem2  19398  ioombl1  19444  ioorf  19453  ioorval  19454  ioorinv2  19455  uniioombllem6  19468  dyadval  19472  opnmbl  19482  mbfimaopnlem  19535  limccnp2  19767  dvdsmulf1o  20967  hhssnvt  22753  hhsssh  22757  opfv  24046  xppreima  24047  ofpreima  24069  qqhval2  24354  rrvadd  24698  erdszelem9  24873  erdszelem10  24874  txpcon  24907  txsconlem  24915  sbcopg  25114  mblfinlem  26190  heiborlem6  26462  heiborlem7  26463  heiborlem8  26464  pellexlem3  26831  pellex  26835  aoveq123d  27956  swrdswrd0  28088  swrdccatin12b  28102  swrdccat3b  28106  cshfn  28122  2shwrd1lem1  28136  2shwrd2lem1  28142  bnj1442  29272  bnj1450  29273  bnj1463  29278  bnj1529  29293  dvhvaddcbv  31726  dvhvaddval  31727  dvhopvadd  31730  dvhvaddcomN  31733  dvhvaddass  31734  dvhvscacbv  31735  dvhvscaval  31736  dvhopvsca  31739  dvhgrp  31744  dvhlveclem  31745  dvh0g  31748  dvhopaddN  31751  dvhopspN  31752  dvhopN  31753  cdlemn4  31835  hdmapffval  32466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815
  Copyright terms: Public domain W3C validator