Theorem opeq12d 4857

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

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		opeq12 4851	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  nfopd  4866  moop2  5477  iunopeqop  5496  dfid2  5550  fsn2g  7127  funopsn  7137  fnprb  7199  fntpb  7200  fnpr2g  7201  fliftfuns  7306  dfmpo  8099  fsplit  8114  fsplitfpar  8115  fnwelem  8128  fimaproj  8132  seqomlem0  8461  seqomlem1  8462  seqomlem4  8465  qliftfuns  8816  xpassen  9078  xpdom2  9079  xpf1o  9151  xpmapenlem  9156  xpmapen  9157  mapunen  9158  xpwdomg  9597  fseqenlem2  10037  nqereu  10941  addpipq2  10948  addpipq  10949  mulpipq2  10951  mulpipq  10952  1nqenq  10974  mulidnq  10975  ltexnq  10987  prlem934  11045  addsrmo  11085  mulsrmo  11086  addsrpr  11087  mulsrpr  11088  mulcnsr  11148  mulresr  11151  axcnre  11176  om2uzrdg  13972  uzrdgsuci  13976  pfxsuff1eqwrdeq  14715  swrdpfx  14723  ccatopth  14732  swrdccatin2d  14760  splval  14767  splcl  14768  cshfn  14806  repswcshw  14828  2swrd2eqwrdeq  14970  ruclem1  16247  eucalgval2  16598  qnumdenbi  16761  crth  16795  phimullem  16796  prmreclem3  16936  setsstruct  17193  ressval3d  17265  imasval  17523  imasaddvallem  17541  xpsff1o  17579  catidex  17684  cidval  17687  catcocl  17695  catass  17696  oppccofval  17726  sectfval  17762  subccocl  17856  isfunc  17875  funcco  17882  idfuval  17887  idfucl  17892  cofuval  17893  cofuval2  17898  cofucl  17899  cofuass  17900  cofulid  17901  cofurid  17902  resfval  17903  resfval2  17904  funcres  17907  inclfusubc  17954  isnat  17961  nati  17969  fucco  17976  fuccoval  17977  coaval  18079  catcisolem  18121  xpcval  18187  xpcco  18193  xpcco2  18197  xpccatid  18198  xpcid  18199  1stfval  18201  2ndfval  18204  1stfcl  18207  2ndfcl  18208  prfval  18209  prf1  18210  prf2fval  18211  prf2  18212  prfcl  18213  prf1st  18214  prf2nd  18215  1st2ndprf  18216  xpcpropd  18218  evlfval  18227  evlf2  18228  evlfcllem  18231  evlfcl  18232  curfval  18233  curf1  18235  curf1cl  18238  curf2cl  18241  curfcl  18242  curfpropd  18243  uncf1  18246  uncf2  18247  curfuncf  18248  uncfcurf  18249  diagval  18250  curf2ndf  18257  hofval  18262  hof2fval  18265  hofcl  18269  yonval  18271  hofpropd  18277  yonedalem21  18283  yonedalem22  18288  yonedalem3  18290  xpsmnd0  18754  xpsinv  19041  xpsgrpsub  19042  symg2bas  19372  xpsring1d  20291  funcrngcsetc  20598  funcrngcsetcALT  20599  funcringcsetc  20632  rngqiprngimfv  21257  rngqiprngghm  21258  rngqiprngimf1  21259  rngqiprngimfo  21260  rngqiprnglin  21261  rngqipring1  21275  rngqiprngfu  21276  pzriprnglem6  21445  pzriprnglem12  21451  mat1dimmul  22412  txcnp  23556  upxp  23559  uptx  23561  hauseqlcld  23582  txlm  23584  txkgen  23588  cnmpt1t  23601  cnmpt2t  23609  txhmeo  23739  flfcnp2  23943  ucnimalem  24216  ucnima  24217  fmucndlem  24227  fmucnd  24228  cnheiborlem  24902  pi1xfrcnvlem  25005  ovollb2lem  25439  ovollb2  25440  ovolshftlem2  25461  ovolscalem2  25465  ioombl1  25513  ioorf  25524  ioorval  25525  ioorinv2  25526  uniioombllem6  25539  dyadval  25543  opnmbl  25553  mbfimaopnlem  25606  limccnp2  25843  mpodvdsmulf1o  27154  dvdsmulf1o  27156  precsexlemcbv  28147  precsexlem3  28150  seqseq123d  28209  om2noseqrdg  28227  noseqrdgsuc  28231  ebtwntg  28907  numclwwlk1lem2fv  30283  numclwwlk1lem2fo  30285  numclwwlk1lem2  30287  wlkl0  30294  hhssnvt  31192  hhsssh  31196  opsbc2ie  32403  opreu2reuALT  32404  opfv  32568  xppreima  32569  2ndresdju  32573  aciunf1lem  32586  ofpreima  32589  fgreu  32596  gsumwrd2dccatlem  33006  gsumwrd2dccat  33007  rlocval  33200  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rloc0g  33212  rloc1r  33213  rlocf1  33214  zringfrac  33515  smatlem  33774  qtophaus  33813  qqhval2  33959  esum2dlem  34069  rrvadd  34430  hgt750lemb  34634  bnj1442  35026  bnj1450  35027  bnj1463  35032  bnj1529  35047  swrdrevpfx  35085  erdszelem9  35167  erdszelem10  35168  txpconn  35200  txsconnlem  35208  goaleq12d  35319  msubval  35493  msubco  35499  mvhval  35502  msubvrs  35528  cbvoprab123vw  36203  cbvoprab23vw  36204  cbvoprab13vw  36205  cbvopabdavw  36230  cbvoprab123davw  36238  cbvoprab12davw  36239  cbvoprab23davw  36240  cbvoprab13davw  36241  bj-dfid2ALT  37029  bj-endval  37279  finxpreclem3  37357  poimirlem4  37594  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  heiborlem6  37786  heiborlem7  37787  heiborlem8  37788  nfopdALT  38935  dvhvaddcbv  41054  dvhvaddval  41055  dvhopvadd  41058  dvhvaddcomN  41061  dvhvaddass  41062  dvhvscacbv  41063  dvhvscaval  41064  dvhopvsca  41067  dvhgrp  41072  dvhlveclem  41073  dvh0g  41076  dvhopaddN  41079  dvhopspN  41080  dvhopN  41081  cdlemn4  41163  hdmapffval  41791  pellexlem3  42801  pellex  42805  elcnvlem  43572  dvnprodlem1  45923  dvnprodlem3  45925  etransclem44  46255  ovolval4  46628  ovolval5lem3  46631  aoveq123d  47155  prproropf1olem2  47466  prproropf1olem3  47467  prproropf1olem4  47468  prproropf1o  47469  prproropreud  47471  isisubgr  47823  eloprab1st2nd  48791  ssccatid  48987  oppfvalg  49022  imaf1co  49043  xpcfucco3  49123  dfswapf2  49126  swapfval  49127  swapfcoa  49146  tposcurf1  49158  diag1  49163  fuco2eld2  49173  fucofvalg  49177  fuco21  49195  fuco11bALT  49197  fuco23  49200  fuco22natlem3  49203  fuco22nat  49205  fucoid  49207  fuco22a  49209  fucocolem2  49213  fucocolem4  49215  postcofval  49223  precofval  49226  precofvalALT  49227  precofval3  49230  prcofvalg  49235  termcfuncval  49365  diag1f1olem  49366  mndtcval  49404  mndtcco  49410  2arwcatlem2  49421  2arwcatlem3  49422  2arwcatlem4  49423  2arwcat  49425  setc1onsubc  49427  lanfval  49438  ranfval  49439  ranup  49464  concom  49481  islmd  49483