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

Theorem opeq12d 4805
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 4799 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3syl2anc 584 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cop 4565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566
This theorem is referenced by:  nfopd  4814  moop2  5384  iunopeqop  5403  fsn2g  6893  funopsn  6903  fnprb  6963  fntpb  6964  fnpr2g  6965  fliftfuns  7056  dfmpo  7788  fsplit  7803  fsplitOLD  7804  fsplitfpar  7805  fnwelem  7816  fimaproj  7820  seqomlem0  8076  seqomlem1  8077  seqomlem4  8080  qliftfuns  8374  xpassen  8600  xpdom2  8601  xpf1o  8668  xpmapenlem  8673  xpmapen  8674  mapunen  8675  xpwdomg  9038  fseqenlem2  9440  nqereu  10340  addpipq2  10347  addpipq  10348  mulpipq2  10350  mulpipq  10351  1nqenq  10373  mulidnq  10374  ltexnq  10386  prlem934  10444  addsrmo  10484  mulsrmo  10485  addsrpr  10486  mulsrpr  10487  mulcnsr  10547  mulresr  10550  axcnre  10575  om2uzrdg  13314  uzrdgsuci  13318  pfxsuff1eqwrdeq  14051  swrdpfx  14059  ccatopth  14068  swrdccatin2d  14096  splval  14103  splcl  14104  cshfn  14142  repswcshw  14164  2swrd2eqwrdeq  14305  ruclem1  15574  eucalgval2  15915  qnumdenbi  16074  crth  16105  phimullem  16106  prmreclem3  16244  setsstruct  16513  ressval3d  16551  imasval  16774  imasaddvallem  16792  xpsff1o  16830  catidex  16935  cidval  16938  catcocl  16946  catass  16947  oppccofval  16976  sectfval  17011  subccocl  17105  isfunc  17124  funcco  17131  idfuval  17136  idfucl  17141  cofuval  17142  cofuval2  17147  cofucl  17148  cofuass  17149  cofulid  17150  cofurid  17151  resfval  17152  resfval2  17153  funcres  17156  isnat  17207  nati  17215  fucco  17222  fuccoval  17223  coaval  17318  catcisolem  17356  xpcval  17417  xpcco  17423  xpcco2  17427  xpccatid  17428  xpcid  17429  1stfval  17431  2ndfval  17434  1stfcl  17437  2ndfcl  17438  prfval  17439  prf1  17440  prf2fval  17441  prf2  17442  prfcl  17443  prf1st  17444  prf2nd  17445  1st2ndprf  17446  xpcpropd  17448  evlfval  17457  evlf2  17458  evlfcllem  17461  evlfcl  17462  curfval  17463  curf1  17465  curf1cl  17468  curf2cl  17471  curfcl  17472  curfpropd  17473  uncf1  17476  uncf2  17477  curfuncf  17478  uncfcurf  17479  diagval  17480  curf2ndf  17487  hofval  17492  hof2fval  17495  hofcl  17499  yonval  17501  hofpropd  17507  yonedalem21  17513  yonedalem22  17518  yonedalem3  17520  symg2bas  18457  mat1dimmul  21015  txcnp  22158  upxp  22161  uptx  22163  hauseqlcld  22184  txlm  22186  txkgen  22190  cnmpt1t  22203  cnmpt2t  22211  txhmeo  22341  flfcnp2  22545  ucnimalem  22818  ucnima  22819  fmucndlem  22829  fmucnd  22830  cnheiborlem  23487  pi1xfrcnvlem  23589  ovollb2lem  24018  ovollb2  24019  ovolshftlem2  24040  ovolscalem2  24044  ioombl1  24092  ioorf  24103  ioorval  24104  ioorinv2  24105  uniioombllem6  24118  dyadval  24122  opnmbl  24132  mbfimaopnlem  24185  limccnp2  24419  dvdsmulf1o  25699  ebtwntg  26696  numclwwlk1lem2fv  28063  numclwwlk1lem2fo  28065  numclwwlk1lem2  28067  wlkl0  28074  hhssnvt  28970  hhsssh  28974  opsbc2ie  30167  opreu2reuALT  30168  opfv  30322  xppreima  30323  aciunf1lem  30336  ofpreima  30339  fgreu  30346  smatlem  30962  qtophaus  31000  qqhval2  31123  esum2dlem  31251  rrvadd  31610  hgt750lemb  31827  bnj1442  32219  bnj1450  32220  bnj1463  32225  bnj1529  32240  swrdrevpfx  32261  erdszelem9  32344  erdszelem10  32345  txpconn  32377  txsconnlem  32385  goaleq12d  32496  msubval  32670  msubco  32676  mvhval  32679  msubvrs  32705  finxpreclem3  34557  poimirlem4  34778  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  heiborlem6  34977  heiborlem7  34978  heiborlem8  34979  nfopdALT  35989  dvhvaddcbv  38107  dvhvaddval  38108  dvhopvadd  38111  dvhvaddcomN  38114  dvhvaddass  38115  dvhvscacbv  38116  dvhvscaval  38117  dvhopvsca  38120  dvhgrp  38125  dvhlveclem  38126  dvh0g  38129  dvhopaddN  38132  dvhopspN  38133  dvhopN  38134  cdlemn4  38216  hdmapffval  38844  pellexlem3  39308  pellex  39312  elcnvlem  39841  dvnprodlem1  42111  dvnprodlem3  42113  etransclem44  42444  ovolval4  42814  ovolval5lem3  42817  aoveq123d  43258  prproropf1olem2  43513  prproropf1olem3  43514  prproropf1olem4  43515  prproropf1o  43516  prproropreud  43518  inclfusubc  44036  funcrngcsetc  44167  funcrngcsetcALT  44168  funcringcsetc  44204
  Copyright terms: Public domain W3C validator