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

Theorem opeq12d 4133
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 4127 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 665 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437   <.cop 3942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943
This theorem is referenced by:  nfopd  4142  csbopg  4143  moop2  4653  fsn2g  6018  fnprb  6077  fnpr2g  6078  fliftfuns  6161  dfmpt2  6836  fsplit  6851  fnwelem  6861  seqomlem0  7116  seqomlem1  7117  seqomlem4  7120  qliftfuns  7400  xpassen  7614  xpdom2  7615  xpf1o  7682  xpmapenlem  7687  xpmapen  7688  mapunen  7689  xpwdomg  8048  fseqenlem2  8402  nqereu  9300  addpipq2  9307  addpipq  9308  mulpipq2  9310  mulpipq  9311  1nqenq  9333  mulidnq  9334  ltexnq  9346  prlem934  9404  addsrmo  9443  mulsrmo  9444  addsrpr  9445  mulsrpr  9446  mulcnsr  9506  mulresr  9509  axcnre  9534  om2uzrdg  12115  uzrdgsuci  12119  2swrd1eqwrdeq  12751  swrdswrd0  12759  ccatopth  12767  swrdccatin2d  12797  splval  12799  splcl  12800  cshfn  12833  repswcshw  12852  2swrd2eqwrdeq  12967  ruclem1  14221  eucalgval2  14478  qnumdenbi  14631  crt  14664  phimullem  14665  prmreclem3  14800  ressval3d  15124  imasval  15349  imasvalOLD  15350  imasaddvallem  15373  xpsff1o  15412  catidex  15518  cidval  15521  catcocl  15529  catass  15530  oppccofval  15559  sectfval  15594  subccocl  15688  isfunc  15707  funcco  15714  idfuval  15719  idfucl  15724  cofuval  15725  cofuval2  15730  cofucl  15731  cofuass  15732  cofulid  15733  cofurid  15734  resfval  15735  resfval2  15736  funcres  15739  isnat  15790  nati  15798  fucco  15805  fuccoval  15806  coaval  15901  catcisolem  15939  xpcval  16000  xpcco  16006  xpcco2  16010  xpccatid  16011  xpcid  16012  1stfval  16014  2ndfval  16017  1stfcl  16020  2ndfcl  16021  prfval  16022  prf1  16023  prf2fval  16024  prf2  16025  prfcl  16026  prf1st  16027  prf2nd  16028  1st2ndprf  16029  xpcpropd  16031  evlfval  16040  evlf2  16041  evlfcllem  16044  evlfcl  16045  curfval  16046  curf1  16048  curf1cl  16051  curf2cl  16054  curfcl  16055  curfpropd  16056  uncf1  16059  uncf2  16060  curfuncf  16061  uncfcurf  16062  diagval  16063  curf2ndf  16070  hofval  16075  hof2fval  16078  hofcl  16082  yonval  16084  hofpropd  16090  yonedalem21  16096  yonedalem22  16101  yonedalem3  16103  symg2bas  16977  mat1dimmul  19438  txcnp  20572  upxp  20575  uptx  20577  hauseqlcld  20598  txlm  20600  txkgen  20604  cnmpt1t  20617  cnmpt2t  20625  txhmeo  20755  pt1hmeo  20758  flfcnp2  20959  ucnimalem  21232  ucnima  21233  fmucndlem  21243  fmucnd  21244  cnheiborlem  21919  pi1xfrcnvlem  22024  ovollb2lem  22378  ovollb2  22379  ovolshftlem2  22400  ovolscalem2  22404  ioombl1  22452  ioorf  22462  ioorval  22463  ioorinv2  22464  ioorfOLD  22467  ioorvalOLD  22468  ioorinv2OLD  22469  uniioombllem6  22483  dyadval  22487  opnmbl  22497  mbfimaopnlem  22548  limccnp2  22784  dvdsmulf1o  24060  ebtwntg  24949  usgrac  25015  numclwlk1lem2fv  25758  numclwlk1lem2fo  25760  hhssnvt  26853  hhsssh  26857  opfv  28188  xppreima  28189  aciunf1lem  28205  ofpreima  28209  fgreu  28215  smatlem  28570  fimaproj  28607  qtophaus  28610  qqhval2  28733  esum2dlem  28860  rrvadd  29232  bnj1442  29805  bnj1450  29806  bnj1463  29811  bnj1529  29826  erdszelem9  29869  erdszelem10  29870  txpcon  29902  txsconlem  29910  msubval  30110  msubco  30116  mvhval  30119  msubvrs  30145  finxpreclem3  31692  poimirlem4  31851  opnmbllem0  31883  mblfinlem1  31884  mblfinlem2  31885  heiborlem6  32055  heiborlem7  32056  heiborlem8  32057  dvhvaddcbv  34569  dvhvaddval  34570  dvhopvadd  34573  dvhvaddcomN  34576  dvhvaddass  34577  dvhvscacbv  34578  dvhvscaval  34579  dvhopvsca  34582  dvhgrp  34587  dvhlveclem  34588  dvh0g  34591  dvhopaddN  34594  dvhopspN  34595  dvhopN  34596  cdlemn4  34678  hdmapffval  35309  pellexlem3  35588  pellex  35592  elcnvlem  36120  dvnprodlem1  37704  dvnprodlem3  37706  etransclem44  38026  aoveq123d  38493  pfxsuff1eqwrdeq  38761  iunopeqop  38813  funopsn  38824  inclfusubc  39458  funcrngcsetc  39591  funcrngcsetcALT  39592  funcringcsetc  39628
  Copyright terms: Public domain W3C validator