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

Theorem opeq12d 4221
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 4215 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 661 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379   <.cop 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034
This theorem is referenced by:  nfopd  4230  csbopg  4231  moop2  4742  fnprb  6117  fliftfuns  6198  dfmpt2  6870  fsplit  6885  fnwelem  6895  seqomlem0  7111  seqomlem1  7112  seqomlem4  7115  qliftfuns  7395  xpassen  7608  xpdom2  7609  xpf1o  7676  xpmapenlem  7681  xpmapen  7682  mapunen  7683  xpwdomg  8007  fseqenlem2  8402  nqereu  9303  addpipq2  9310  addpipq  9311  mulpipq2  9313  mulpipq  9314  1nqenq  9336  mulidnq  9337  ltexnq  9349  prlem934  9407  addsrmo  9446  mulsrmo  9447  addsrpr  9448  mulsrpr  9449  mulcnsr  9509  mulresr  9512  axcnre  9537  om2uzrdg  12030  uzrdgsuci  12034  2swrd1eqwrdeq  12636  swrdswrd0  12644  ccatopth  12652  swrdccatin2d  12682  splval  12684  splcl  12685  cshfn  12718  repswcshw  12737  2swrd2eqwrdeq  12848  ruclem1  13818  eucalgval2  14062  qnumdenbi  14129  crt  14160  phimullem  14161  prmreclem3  14288  imasval  14759  imasaddvallem  14777  xpsff1o  14816  catidex  14922  cidval  14925  catcocl  14933  catass  14934  oppccofval  14965  sectfval  15000  subccocl  15065  isfunc  15084  funcco  15091  idfuval  15096  idfucl  15101  cofuval  15102  cofuval2  15107  cofucl  15108  cofuass  15109  cofulid  15110  cofurid  15111  resfval  15112  resfval2  15113  funcres  15116  isnat  15167  nati  15175  fucco  15182  fuccoval  15183  coaval  15246  catcisolem  15284  xpcval  15297  xpcco  15303  xpcco2  15307  xpccatid  15308  xpcid  15309  1stfval  15311  2ndfval  15314  1stfcl  15317  2ndfcl  15318  prfval  15319  prf1  15320  prf2fval  15321  prf2  15322  prfcl  15323  prf1st  15324  prf2nd  15325  1st2ndprf  15326  xpcpropd  15328  evlfval  15337  evlf2  15338  evlfcllem  15341  evlfcl  15342  curfval  15343  curf1  15345  curf1cl  15348  curf2cl  15351  curfcl  15352  curfpropd  15353  uncf1  15356  uncf2  15357  curfuncf  15358  uncfcurf  15359  diagval  15360  curf2ndf  15367  hofval  15372  hof2fval  15375  hofcl  15379  yonval  15381  hofpropd  15387  yonedalem21  15393  yonedalem22  15398  yonedalem3  15400  symg2bas  16215  mat1dimmul  18742  txcnp  19853  upxp  19856  uptx  19858  hauseqlcld  19879  txlm  19881  txkgen  19885  cnmpt1t  19898  cnmpt2t  19906  txhmeo  20036  pt1hmeo  20039  flfcnp2  20240  ucnimalem  20515  ucnima  20516  fmucndlem  20526  fmucnd  20527  cnheiborlem  21186  pi1xfrcnvlem  21288  ovollb2lem  21631  ovollb2  21632  ovolshftlem2  21653  ovolscalem2  21657  ioombl1  21704  ioorf  21714  ioorval  21715  ioorinv2  21716  uniioombllem6  21729  dyadval  21733  opnmbl  21743  mbfimaopnlem  21794  limccnp2  22028  dvdsmulf1o  23195  ebtwntg  23958  usgrac  24024  numclwlk1lem2fv  24767  numclwlk1lem2fo  24769  hhssnvt  25854  hhsssh  25858  opfv  27155  xppreima  27156  ofpreima  27176  fgreu  27182  fimaproj  27496  qqhval2  27596  qtophaus  27634  rrvadd  28028  erdszelem9  28280  erdszelem10  28281  txpcon  28314  txsconlem  28322  opnmbllem0  29625  mblfinlem1  29626  mblfinlem2  29627  heiborlem6  29913  heiborlem7  29914  heiborlem8  29915  pellexlem3  30369  pellex  30373  aoveq123d  31730  bnj1442  33184  bnj1450  33185  bnj1463  33190  bnj1529  33205  dvhvaddcbv  35886  dvhvaddval  35887  dvhopvadd  35890  dvhvaddcomN  35893  dvhvaddass  35894  dvhvscacbv  35895  dvhvscaval  35896  dvhopvsca  35899  dvhgrp  35904  dvhlveclem  35905  dvh0g  35908  dvhopaddN  35911  dvhopspN  35912  dvhopN  35913  cdlemn4  35995  hdmapffval  36626
  Copyright terms: Public domain W3C validator