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

Theorem opeq12d 4342
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 (𝜑𝐴 = 𝐵)
opeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
opeq12d (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Proof of Theorem opeq12d
StepHypRef Expression
1 opeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opeq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 opeq12 4336 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3syl2anc 690 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cop 4130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131
This theorem is referenced by:  nfopd  4351  moop2  4884  fsn2g  6295  fnprb  6354  fntpb  6355  fnpr2g  6356  fliftfuns  6441  dfmpt2  7131  fsplit  7146  fnwelem  7156  seqomlem0  7408  seqomlem1  7409  seqomlem4  7412  qliftfuns  7698  xpassen  7916  xpdom2  7917  xpf1o  7984  xpmapenlem  7989  xpmapen  7990  mapunen  7991  xpwdomg  8350  fseqenlem2  8708  nqereu  9607  addpipq2  9614  addpipq  9615  mulpipq2  9617  mulpipq  9618  1nqenq  9640  mulidnq  9641  ltexnq  9653  prlem934  9711  addsrmo  9750  mulsrmo  9751  addsrpr  9752  mulsrpr  9753  mulcnsr  9813  mulresr  9816  axcnre  9841  om2uzrdg  12574  uzrdgsuci  12578  2swrd1eqwrdeq  13254  swrdswrd0  13262  ccatopth  13270  swrdccatin2d  13299  splval  13301  splcl  13302  cshfn  13335  repswcshw  13357  2swrd2eqwrdeq  13492  ruclem1  14747  eucalgval2  15080  qnumdenbi  15238  crth  15269  phimullem  15270  prmreclem3  15408  ressval3d  15712  imasval  15942  imasaddvallem  15960  xpsff1o  15999  catidex  16106  cidval  16109  catcocl  16117  catass  16118  oppccofval  16147  sectfval  16182  subccocl  16276  isfunc  16295  funcco  16302  idfuval  16307  idfucl  16312  cofuval  16313  cofuval2  16318  cofucl  16319  cofuass  16320  cofulid  16321  cofurid  16322  resfval  16323  resfval2  16324  funcres  16327  isnat  16378  nati  16386  fucco  16393  fuccoval  16394  coaval  16489  catcisolem  16527  xpcval  16588  xpcco  16594  xpcco2  16598  xpccatid  16599  xpcid  16600  1stfval  16602  2ndfval  16605  1stfcl  16608  2ndfcl  16609  prfval  16610  prf1  16611  prf2fval  16612  prf2  16613  prfcl  16614  prf1st  16615  prf2nd  16616  1st2ndprf  16617  xpcpropd  16619  evlfval  16628  evlf2  16629  evlfcllem  16632  evlfcl  16633  curfval  16634  curf1  16636  curf1cl  16639  curf2cl  16642  curfcl  16643  curfpropd  16644  uncf1  16647  uncf2  16648  curfuncf  16649  uncfcurf  16650  diagval  16651  curf2ndf  16658  hofval  16663  hof2fval  16666  hofcl  16670  yonval  16672  hofpropd  16678  yonedalem21  16684  yonedalem22  16689  yonedalem3  16691  symg2bas  17589  mat1dimmul  20048  txcnp  21180  upxp  21183  uptx  21185  hauseqlcld  21206  txlm  21208  txkgen  21212  cnmpt1t  21225  cnmpt2t  21233  txhmeo  21363  flfcnp2  21568  ucnimalem  21841  ucnima  21842  fmucndlem  21852  fmucnd  21853  cnheiborlem  22508  pi1xfrcnvlem  22611  ovollb2lem  23007  ovollb2  23008  ovolshftlem2  23029  ovolscalem2  23033  ioombl1  23081  ioorf  23091  ioorval  23092  ioorinv2  23093  uniioombllem6  23106  dyadval  23110  opnmbl  23120  mbfimaopnlem  23172  limccnp2  23406  dvdsmulf1o  24664  ebtwntg  25607  usgrac  25673  numclwlk1lem2fv  26413  numclwlk1lem2fo  26415  hhssnvt  27299  hhsssh  27303  opfv  28621  xppreima  28622  aciunf1lem  28637  ofpreima  28641  fgreu  28647  smatlem  28984  fimaproj  29021  qtophaus  29024  qqhval2  29147  esum2dlem  29274  rrvadd  29634  bnj1442  30164  bnj1450  30165  bnj1463  30170  bnj1529  30185  erdszelem9  30228  erdszelem10  30229  txpcon  30261  txsconlem  30269  msubval  30469  msubco  30475  mvhval  30478  msubvrs  30504  finxpreclem3  32189  poimirlem4  32366  opnmbllem0  32398  mblfinlem1  32399  mblfinlem2  32400  heiborlem6  32568  heiborlem7  32569  heiborlem8  32570  nfopdALT  33059  dvhvaddcbv  35179  dvhvaddval  35180  dvhopvadd  35183  dvhvaddcomN  35186  dvhvaddass  35187  dvhvscacbv  35188  dvhvscaval  35189  dvhopvsca  35192  dvhgrp  35197  dvhlveclem  35198  dvh0g  35201  dvhopaddN  35204  dvhopspN  35205  dvhopN  35206  cdlemn4  35288  hdmapffval  35919  pellexlem3  36196  pellex  36200  elcnvlem  36709  dvnprodlem1  38619  dvnprodlem3  38621  etransclem44  38954  ovolval4  39324  ovolval5lem3  39327  aoveq123d  39691  pfxsuff1eqwrdeq  40054  iunopeqop  40110  funopsn  40123  av-numclwlk1lem2fv  41504  av-numclwlk1lem2fo  41506  inclfusubc  41638  funcrngcsetc  41771  funcrngcsetcALT  41772  funcringcsetc  41808
  Copyright terms: Public domain W3C validator