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

Theorem opeq12d 4441
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 4435 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
41, 2, 3syl2anc 694 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cop 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217
This theorem is referenced by:  nfopd  4450  moop2  4995  iunopeqop  5010  fsn2g  6445  funopsn  6453  fnprb  6513  fntpb  6514  fnpr2g  6515  fliftfuns  6604  dfmpt2  7312  fsplit  7327  fnwelem  7337  seqomlem0  7589  seqomlem1  7590  seqomlem4  7593  qliftfuns  7877  xpassen  8095  xpdom2  8096  xpf1o  8163  xpmapenlem  8168  xpmapen  8169  mapunen  8170  xpwdomg  8531  fseqenlem2  8886  nqereu  9789  addpipq2  9796  addpipq  9797  mulpipq2  9799  mulpipq  9800  1nqenq  9822  mulidnq  9823  ltexnq  9835  prlem934  9893  addsrmo  9932  mulsrmo  9933  addsrpr  9934  mulsrpr  9935  mulcnsr  9995  mulresr  9998  axcnre  10023  om2uzrdg  12795  uzrdgsuci  12799  2swrd1eqwrdeq  13500  swrdswrd0  13508  ccatopth  13516  swrdccatin2d  13546  splval  13548  splcl  13549  cshfn  13582  repswcshw  13604  2swrd2eqwrdeq  13742  ruclem1  15004  eucalgval2  15341  qnumdenbi  15499  crth  15530  phimullem  15531  prmreclem3  15669  setsstruct  15945  ressval3d  15984  imasval  16218  imasaddvallem  16236  xpsff1o  16275  catidex  16382  cidval  16385  catcocl  16393  catass  16394  oppccofval  16423  sectfval  16458  subccocl  16552  isfunc  16571  funcco  16578  idfuval  16583  idfucl  16588  cofuval  16589  cofuval2  16594  cofucl  16595  cofuass  16596  cofulid  16597  cofurid  16598  resfval  16599  resfval2  16600  funcres  16603  isnat  16654  nati  16662  fucco  16669  fuccoval  16670  coaval  16765  catcisolem  16803  xpcval  16864  xpcco  16870  xpcco2  16874  xpccatid  16875  xpcid  16876  1stfval  16878  2ndfval  16881  1stfcl  16884  2ndfcl  16885  prfval  16886  prf1  16887  prf2fval  16888  prf2  16889  prfcl  16890  prf1st  16891  prf2nd  16892  1st2ndprf  16893  xpcpropd  16895  evlfval  16904  evlf2  16905  evlfcllem  16908  evlfcl  16909  curfval  16910  curf1  16912  curf1cl  16915  curf2cl  16918  curfcl  16919  curfpropd  16920  uncf1  16923  uncf2  16924  curfuncf  16925  uncfcurf  16926  diagval  16927  curf2ndf  16934  hofval  16939  hof2fval  16942  hofcl  16946  yonval  16948  hofpropd  16954  yonedalem21  16960  yonedalem22  16965  yonedalem3  16967  symg2bas  17864  mat1dimmul  20330  txcnp  21471  upxp  21474  uptx  21476  hauseqlcld  21497  txlm  21499  txkgen  21503  cnmpt1t  21516  cnmpt2t  21524  txhmeo  21654  flfcnp2  21858  ucnimalem  22131  ucnima  22132  fmucndlem  22142  fmucnd  22143  cnheiborlem  22800  pi1xfrcnvlem  22902  ovollb2lem  23302  ovollb2  23303  ovolshftlem2  23324  ovolscalem2  23328  ioombl1  23376  ioorf  23387  ioorval  23388  ioorinv2  23389  uniioombllem6  23402  dyadval  23406  opnmbl  23416  mbfimaopnlem  23467  limccnp2  23701  dvdsmulf1o  24965  ebtwntg  25907  numclwlk1lem2fv  27346  numclwlk1lem2fo  27348  numclwlk1lem2  27350  hhssnvt  28250  hhsssh  28254  opfv  29576  xppreima  29577  aciunf1lem  29590  ofpreima  29593  fgreu  29599  smatlem  29991  fimaproj  30028  qtophaus  30031  qqhval2  30154  esum2dlem  30282  rrvadd  30642  hgt750lemb  30862  bnj1442  31243  bnj1450  31244  bnj1463  31249  bnj1529  31264  erdszelem9  31307  erdszelem10  31308  txpconn  31340  txsconnlem  31348  msubval  31548  msubco  31554  mvhval  31557  msubvrs  31583  finxpreclem3  33360  poimirlem4  33543  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  heiborlem6  33745  heiborlem7  33746  heiborlem8  33747  nfopdALT  34576  dvhvaddcbv  36695  dvhvaddval  36696  dvhopvadd  36699  dvhvaddcomN  36702  dvhvaddass  36703  dvhvscacbv  36704  dvhvscaval  36705  dvhopvsca  36708  dvhgrp  36713  dvhlveclem  36714  dvh0g  36717  dvhopaddN  36720  dvhopspN  36721  dvhopN  36722  cdlemn4  36804  hdmapffval  37435  pellexlem3  37712  pellex  37716  elcnvlem  38224  dvnprodlem1  40479  dvnprodlem3  40481  etransclem44  40813  ovolval4  41186  ovolval5lem3  41189  aoveq123d  41579  pfxsuff1eqwrdeq  41732  inclfusubc  42192  funcrngcsetc  42323  funcrngcsetcALT  42324  funcringcsetc  42360
  Copyright terms: Public domain W3C validator