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

Theorem opeq12d 3820
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 3814 . 2  |-  ( ( A  =  B  /\  C  =  D )  -> 
<. A ,  C >.  = 
<. B ,  D >. )
41, 2, 3syl2anc 642 1  |-  ( ph  -> 
<. A ,  C >.  = 
<. B ,  D >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   <.cop 3656
This theorem is referenced by:  nfopd  3829  moop2  4277  fliftfuns  5829  dfmpt2  6225  fsplit  6239  fnwelem  6246  seqomlem0  6477  seqomlem1  6478  seqomlem4  6481  qliftfuns  6761  xpassen  6972  xpdom2  6973  xpf1o  7039  xpmapenlem  7044  xpmapen  7045  mapunen  7046  xpwdomg  7315  fseqenlem2  7668  nqereu  8569  addpipq2  8576  addpipq  8577  mulpipq2  8579  mulpipq  8580  1nqenq  8602  mulidnq  8603  ltexnq  8615  prlem934  8673  mulsrpr  8714  mulcnsr  8774  mulresr  8777  axcnre  8802  om2uzrdg  11035  uzrdgsuci  11039  ccatopth  11478  splval  11482  splcl  11483  ruclem1  12525  eucalgval2  12767  qnumdenbi  12831  crt  12862  phimullem  12863  prmreclem3  12981  imasval  13430  imasaddvallem  13447  xpsff1o  13486  catidex  13592  cidval  13595  catcocl  13603  catass  13604  oppccofval  13635  sectfval  13670  subccocl  13735  isfunc  13754  funcco  13761  idfuval  13766  idfucl  13771  cofuval  13772  cofuval2  13777  cofucl  13778  cofuass  13779  cofulid  13780  cofurid  13781  resfval  13782  resfval2  13783  funcres  13786  isnat  13837  nati  13845  fucco  13852  fuccoval  13853  coaval  13916  catcisolem  13954  xpcval  13967  xpcco  13973  xpcco2  13977  xpccatid  13978  xpcid  13979  1stfval  13981  2ndfval  13984  1stfcl  13987  2ndfcl  13988  prfval  13989  prf1  13990  prf2fval  13991  prf2  13992  prfcl  13993  prf1st  13994  prf2nd  13995  1st2ndprf  13996  xpcpropd  13998  evlfval  14007  evlf2  14008  evlfcllem  14011  evlfcl  14012  curfval  14013  curf1  14015  curf1cl  14018  curf2cl  14021  curfcl  14022  curfpropd  14023  uncf1  14026  uncf2  14027  curfuncf  14028  uncfcurf  14029  diagval  14030  curf2ndf  14037  hofval  14042  hof2fval  14045  hofcl  14049  yonval  14051  hofpropd  14057  yonedalem21  14063  yonedalem22  14068  yonedalem3  14070  txcnp  17330  upxp  17333  uptx  17335  hauseqlcld  17356  txlm  17358  txkgen  17362  cnmpt1t  17375  cnmpt2t  17383  txhmeo  17510  pt1hmeo  17513  flfcnp2  17718  cnheiborlem  18468  pi1xfrcnvlem  18570  ovollb2lem  18863  ovollb2  18864  ovolshftlem2  18885  ovolscalem2  18889  ioombl1  18935  ioorf  18944  ioorval  18945  ioorinv2  18946  uniioombllem6  18959  dyadval  18963  opnmbl  18973  mbfimaopnlem  19026  limccnp2  19258  dvdsmulf1o  20450  hhssnvt  21858  hhsssh  21862  opfv  23206  xppreima  23226  erdszelem9  23745  erdszelem10  23746  txpcon  23778  txsconlem  23786  sbcopg  24037  11st22nd  25148  eloi  25189  cbicp  25269  isder  25810  homib  25899  idsubfun  25961  idmor  26049  cmp2morp  26061  cmp2morpcats  26064  cmpmorass  26069  morexcmp  26070  cmpidmor2  26072  cmpidmor3  26073  iscatset  26081  heiborlem6  26643  heiborlem7  26644  heiborlem8  26645  pellexlem3  27019  pellex  27023  matval  27568  aoveq123d  28146  bnj1442  29395  bnj1450  29396  bnj1463  29401  bnj1529  29416  dvhvaddcbv  31901  dvhvaddval  31902  dvhopvadd  31905  dvhvaddcomN  31908  dvhvaddass  31909  dvhvscacbv  31910  dvhvscaval  31911  dvhopvsca  31914  dvhgrp  31919  dvhlveclem  31920  dvh0g  31923  dvhopaddN  31926  dvhopspN  31927  dvhopN  31928  cdlemn4  32010  hdmapffval  32641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662
  Copyright terms: Public domain W3C validator