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

Theorem opeq12d 3927
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 3921 . 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 3753
This theorem is referenced by:  nfopd  3936  moop2  4385  fliftfuns  5968  dfmpt2  6369  fsplit  6383  fnwelem  6390  seqomlem0  6635  seqomlem1  6636  seqomlem4  6639  qliftfuns  6920  xpassen  7131  xpdom2  7132  xpf1o  7198  xpmapenlem  7203  xpmapen  7204  mapunen  7205  xpwdomg  7479  fseqenlem2  7832  nqereu  8732  addpipq2  8739  addpipq  8740  mulpipq2  8742  mulpipq  8743  1nqenq  8765  mulidnq  8766  ltexnq  8778  prlem934  8836  mulsrpr  8877  mulcnsr  8937  mulresr  8940  axcnre  8965  om2uzrdg  11216  uzrdgsuci  11220  ccatopth  11696  splval  11700  splcl  11701  ruclem1  12750  eucalgval2  12992  qnumdenbi  13056  crt  13087  phimullem  13088  prmreclem3  13206  imasval  13657  imasaddvallem  13674  xpsff1o  13713  catidex  13819  cidval  13822  catcocl  13830  catass  13831  oppccofval  13862  sectfval  13897  subccocl  13962  isfunc  13981  funcco  13988  idfuval  13993  idfucl  13998  cofuval  13999  cofuval2  14004  cofucl  14005  cofuass  14006  cofulid  14007  cofurid  14008  resfval  14009  resfval2  14010  funcres  14013  isnat  14064  nati  14072  fucco  14079  fuccoval  14080  coaval  14143  catcisolem  14181  xpcval  14194  xpcco  14200  xpcco2  14204  xpccatid  14205  xpcid  14206  1stfval  14208  2ndfval  14211  1stfcl  14214  2ndfcl  14215  prfval  14216  prf1  14217  prf2fval  14218  prf2  14219  prfcl  14220  prf1st  14221  prf2nd  14222  1st2ndprf  14223  xpcpropd  14225  evlfval  14234  evlf2  14235  evlfcllem  14238  evlfcl  14239  curfval  14240  curf1  14242  curf1cl  14245  curf2cl  14248  curfcl  14249  curfpropd  14250  uncf1  14253  uncf2  14254  curfuncf  14255  uncfcurf  14256  diagval  14257  curf2ndf  14264  hofval  14269  hof2fval  14272  hofcl  14276  yonval  14278  hofpropd  14284  yonedalem21  14290  yonedalem22  14295  yonedalem3  14297  txcnp  17566  upxp  17569  uptx  17571  hauseqlcld  17592  txlm  17594  txkgen  17598  cnmpt1t  17611  cnmpt2t  17619  txhmeo  17749  pt1hmeo  17752  flfcnp2  17953  ucnimalem  18224  ucnima  18225  fmucndlem  18235  fmucnd  18236  cnheiborlem  18843  pi1xfrcnvlem  18945  ovollb2lem  19244  ovollb2  19245  ovolshftlem2  19266  ovolscalem2  19270  ioombl1  19316  ioorf  19325  ioorval  19326  ioorinv2  19327  uniioombllem6  19340  dyadval  19344  opnmbl  19354  mbfimaopnlem  19407  limccnp2  19639  dvdsmulf1o  20839  hhssnvt  22606  hhsssh  22610  opfv  23893  xppreima  23894  qqhval2  24158  rrvadd  24482  erdszelem9  24657  erdszelem10  24658  txpcon  24691  txsconlem  24699  sbcopg  24898  heiborlem6  26209  heiborlem7  26210  heiborlem8  26211  pellexlem3  26578  pellex  26582  aoveq123d  27704  bnj1442  28749  bnj1450  28750  bnj1463  28755  bnj1529  28770  dvhvaddcbv  31255  dvhvaddval  31256  dvhopvadd  31259  dvhvaddcomN  31262  dvhvaddass  31263  dvhvscacbv  31264  dvhvscaval  31265  dvhopvsca  31268  dvhgrp  31273  dvhlveclem  31274  dvh0g  31277  dvhopaddN  31280  dvhopspN  31281  dvhopN  31282  cdlemn4  31364  hdmapffval  31995
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759
  Copyright terms: Public domain W3C validator