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

Theorem opeq12d 4776
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 4770 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3syl2anc 587 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cop 4534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535
This theorem is referenced by:  nfopd  4785  moop2  5360  iunopeqop  5379  fsn2g  6881  funopsn  6891  fnprb  6952  fntpb  6953  fnpr2g  6954  fliftfuns  7050  dfmpo  7784  fsplit  7799  fsplitOLD  7800  fsplitfpar  7801  fnwelem  7812  fimaproj  7816  seqomlem0  8072  seqomlem1  8073  seqomlem4  8076  qliftfuns  8371  xpassen  8598  xpdom2  8599  xpf1o  8667  xpmapenlem  8672  xpmapen  8673  mapunen  8674  xpwdomg  9037  fseqenlem2  9440  nqereu  10344  addpipq2  10351  addpipq  10352  mulpipq2  10354  mulpipq  10355  1nqenq  10377  mulidnq  10378  ltexnq  10390  prlem934  10448  addsrmo  10488  mulsrmo  10489  addsrpr  10490  mulsrpr  10491  mulcnsr  10551  mulresr  10554  axcnre  10579  om2uzrdg  13323  uzrdgsuci  13327  pfxsuff1eqwrdeq  14056  swrdpfx  14064  ccatopth  14073  swrdccatin2d  14101  splval  14108  splcl  14109  cshfn  14147  repswcshw  14169  2swrd2eqwrdeq  14310  ruclem1  15580  eucalgval2  15919  qnumdenbi  16078  crth  16109  phimullem  16110  prmreclem3  16248  setsstruct  16519  ressval3d  16557  imasval  16780  imasaddvallem  16798  xpsff1o  16836  catidex  16941  cidval  16944  catcocl  16952  catass  16953  oppccofval  16982  sectfval  17017  subccocl  17111  isfunc  17130  funcco  17137  idfuval  17142  idfucl  17147  cofuval  17148  cofuval2  17153  cofucl  17154  cofuass  17155  cofulid  17156  cofurid  17157  resfval  17158  resfval2  17159  funcres  17162  isnat  17213  nati  17221  fucco  17228  fuccoval  17229  coaval  17324  catcisolem  17362  xpcval  17423  xpcco  17429  xpcco2  17433  xpccatid  17434  xpcid  17435  1stfval  17437  2ndfval  17440  1stfcl  17443  2ndfcl  17444  prfval  17445  prf1  17446  prf2fval  17447  prf2  17448  prfcl  17449  prf1st  17450  prf2nd  17451  1st2ndprf  17452  xpcpropd  17454  evlfval  17463  evlf2  17464  evlfcllem  17467  evlfcl  17468  curfval  17469  curf1  17471  curf1cl  17474  curf2cl  17477  curfcl  17478  curfpropd  17479  uncf1  17482  uncf2  17483  curfuncf  17484  uncfcurf  17485  diagval  17486  curf2ndf  17493  hofval  17498  hof2fval  17501  hofcl  17505  yonval  17507  hofpropd  17513  yonedalem21  17519  yonedalem22  17524  yonedalem3  17526  symg2bas  18517  mat1dimmul  21085  txcnp  22229  upxp  22232  uptx  22234  hauseqlcld  22255  txlm  22257  txkgen  22261  cnmpt1t  22274  cnmpt2t  22282  txhmeo  22412  flfcnp2  22616  ucnimalem  22890  ucnima  22891  fmucndlem  22901  fmucnd  22902  cnheiborlem  23563  pi1xfrcnvlem  23665  ovollb2lem  24096  ovollb2  24097  ovolshftlem2  24118  ovolscalem2  24122  ioombl1  24170  ioorf  24181  ioorval  24182  ioorinv2  24183  uniioombllem6  24196  dyadval  24200  opnmbl  24210  mbfimaopnlem  24263  limccnp2  24499  dvdsmulf1o  25783  ebtwntg  26780  numclwwlk1lem2fv  28145  numclwwlk1lem2fo  28147  numclwwlk1lem2  28149  wlkl0  28156  hhssnvt  29052  hhsssh  29056  opsbc2ie  30250  opreu2reuALT  30251  opfv  30411  xppreima  30412  2ndresdju  30415  aciunf1lem  30429  ofpreima  30432  fgreu  30439  smatlem  31154  qtophaus  31193  qqhval2  31337  esum2dlem  31465  rrvadd  31824  hgt750lemb  32041  bnj1442  32435  bnj1450  32436  bnj1463  32441  bnj1529  32456  swrdrevpfx  32477  erdszelem9  32560  erdszelem10  32561  txpconn  32593  txsconnlem  32601  goaleq12d  32712  msubval  32886  msubco  32892  mvhval  32895  msubvrs  32921  bj-endval  34730  finxpreclem3  34811  poimirlem4  35060  opnmbllem0  35092  mblfinlem1  35093  mblfinlem2  35094  heiborlem6  35253  heiborlem7  35254  heiborlem8  35255  nfopdALT  36266  dvhvaddcbv  38384  dvhvaddval  38385  dvhopvadd  38388  dvhvaddcomN  38391  dvhvaddass  38392  dvhvscacbv  38393  dvhvscaval  38394  dvhopvsca  38397  dvhgrp  38402  dvhlveclem  38403  dvh0g  38406  dvhopaddN  38409  dvhopspN  38410  dvhopN  38411  cdlemn4  38493  hdmapffval  39121  pellexlem3  39769  pellex  39773  elcnvlem  40298  dvnprodlem1  42585  dvnprodlem3  42587  etransclem44  42917  ovolval4  43287  ovolval5lem3  43290  aoveq123d  43731  prproropf1olem2  44018  prproropf1olem3  44019  prproropf1olem4  44020  prproropf1o  44021  prproropreud  44023  inclfusubc  44488  funcrngcsetc  44619  funcrngcsetcALT  44620  funcringcsetc  44656
  Copyright terms: Public domain W3C validator