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

Theorem opeq12d 3952
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 3946 . 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 1649   <.cop 3777
This theorem is referenced by:  nfopd  3961  moop2  4411  fliftfuns  5995  dfmpt2  6396  fsplit  6410  fnwelem  6420  seqomlem0  6665  seqomlem1  6666  seqomlem4  6669  qliftfuns  6950  xpassen  7161  xpdom2  7162  xpf1o  7228  xpmapenlem  7233  xpmapen  7234  mapunen  7235  xpwdomg  7509  fseqenlem2  7862  nqereu  8762  addpipq2  8769  addpipq  8770  mulpipq2  8772  mulpipq  8773  1nqenq  8795  mulidnq  8796  ltexnq  8808  prlem934  8866  mulsrpr  8907  mulcnsr  8967  mulresr  8970  axcnre  8995  om2uzrdg  11251  uzrdgsuci  11255  ccatopth  11731  splval  11735  splcl  11736  ruclem1  12785  eucalgval2  13027  qnumdenbi  13091  crt  13122  phimullem  13123  prmreclem3  13241  imasval  13692  imasaddvallem  13709  xpsff1o  13748  catidex  13854  cidval  13857  catcocl  13865  catass  13866  oppccofval  13897  sectfval  13932  subccocl  13997  isfunc  14016  funcco  14023  idfuval  14028  idfucl  14033  cofuval  14034  cofuval2  14039  cofucl  14040  cofuass  14041  cofulid  14042  cofurid  14043  resfval  14044  resfval2  14045  funcres  14048  isnat  14099  nati  14107  fucco  14114  fuccoval  14115  coaval  14178  catcisolem  14216  xpcval  14229  xpcco  14235  xpcco2  14239  xpccatid  14240  xpcid  14241  1stfval  14243  2ndfval  14246  1stfcl  14249  2ndfcl  14250  prfval  14251  prf1  14252  prf2fval  14253  prf2  14254  prfcl  14255  prf1st  14256  prf2nd  14257  1st2ndprf  14258  xpcpropd  14260  evlfval  14269  evlf2  14270  evlfcllem  14273  evlfcl  14274  curfval  14275  curf1  14277  curf1cl  14280  curf2cl  14283  curfcl  14284  curfpropd  14285  uncf1  14288  uncf2  14289  curfuncf  14290  uncfcurf  14291  diagval  14292  curf2ndf  14299  hofval  14304  hof2fval  14307  hofcl  14311  yonval  14313  hofpropd  14319  yonedalem21  14325  yonedalem22  14330  yonedalem3  14332  txcnp  17605  upxp  17608  uptx  17610  hauseqlcld  17631  txlm  17633  txkgen  17637  cnmpt1t  17650  cnmpt2t  17658  txhmeo  17788  pt1hmeo  17791  flfcnp2  17992  ucnimalem  18263  ucnima  18264  fmucndlem  18274  fmucnd  18275  cnheiborlem  18932  pi1xfrcnvlem  19034  ovollb2lem  19337  ovollb2  19338  ovolshftlem2  19359  ovolscalem2  19363  ioombl1  19409  ioorf  19418  ioorval  19419  ioorinv2  19420  uniioombllem6  19433  dyadval  19437  opnmbl  19447  mbfimaopnlem  19500  limccnp2  19732  dvdsmulf1o  20932  hhssnvt  22718  hhsssh  22722  opfv  24011  xppreima  24012  ofpreima  24034  qqhval2  24319  rrvadd  24663  erdszelem9  24838  erdszelem10  24839  txpcon  24872  txsconlem  24880  sbcopg  25079  mblfinlem  26143  heiborlem6  26415  heiborlem7  26416  heiborlem8  26417  pellexlem3  26784  pellex  26788  aoveq123d  27909  swrdswrd0  28013  swrdccatin12b  28027  swrdccat3b  28031  bnj1442  29124  bnj1450  29125  bnj1463  29130  bnj1529  29145  dvhvaddcbv  31572  dvhvaddval  31573  dvhopvadd  31576  dvhvaddcomN  31579  dvhvaddass  31580  dvhvscacbv  31581  dvhvscaval  31582  dvhopvsca  31585  dvhgrp  31590  dvhlveclem  31591  dvh0g  31594  dvhopaddN  31597  dvhopspN  31598  dvhopN  31599  cdlemn4  31681  hdmapffval  32312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783
  Copyright terms: Public domain W3C validator