Theorem opeq12d 4825

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 4819	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐷⟩)

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4574

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  nfopd  4834  moop2  5457  iunopeqop  5476  dfid2  5528  fsn2g  7092  funopsn  7102  fnprb  7163  fntpb  7164  fnpr2g  7165  fliftfuns  7269  dfmpo  8052  fsplit  8067  fsplitfpar  8068  fnwelem  8081  fimaproj  8085  seqomlem0  8388  seqomlem1  8389  seqomlem4  8392  qliftfuns  8751  xpassen  9009  xpdom2  9010  xpf1o  9077  xpmapenlem  9082  xpmapen  9083  mapunen  9084  xpwdomg  9500  fseqenlem2  9947  nqereu  10852  addpipq2  10859  addpipq  10860  mulpipq2  10862  mulpipq  10863  1nqenq  10885  mulidnq  10886  ltexnq  10898  prlem934  10956  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  mulcnsr  11059  mulresr  11062  axcnre  11087  om2uzrdg  13918  uzrdgsuci  13922  pfxsuff1eqwrdeq  14661  swrdpfx  14669  ccatopth  14678  swrdccatin2d  14706  splval  14713  splcl  14714  cshfn  14752  repswcshw  14774  2swrd2eqwrdeq  14915  ruclem1  16198  eucalgval2  16550  qnumdenbi  16714  crth  16748  phimullem  16749  prmreclem3  16889  setsstruct  17146  ressval3d  17216  imasval  17475  imasaddvallem  17493  xpsff1o  17531  catidex  17640  cidval  17643  catcocl  17651  catass  17652  oppccofval  17682  sectfval  17718  subccocl  17812  isfunc  17831  funcco  17838  idfuval  17843  idfucl  17848  cofuval  17849  cofuval2  17854  cofucl  17855  cofuass  17856  cofulid  17857  cofurid  17858  resfval  17859  resfval2  17860  funcres  17863  inclfusubc  17910  isnat  17917  nati  17925  fucco  17932  fuccoval  17933  coaval  18035  catcisolem  18077  xpcval  18143  xpcco  18149  xpcco2  18153  xpccatid  18154  xpcid  18155  1stfval  18157  2ndfval  18160  1stfcl  18163  2ndfcl  18164  prfval  18165  prf1  18166  prf2fval  18167  prf2  18168  prfcl  18169  prf1st  18170  prf2nd  18171  1st2ndprf  18172  xpcpropd  18174  evlfval  18183  evlf2  18184  evlfcllem  18187  evlfcl  18188  curfval  18189  curf1  18191  curf1cl  18194  curf2cl  18197  curfcl  18198  curfpropd  18199  uncf1  18202  uncf2  18203  curfuncf  18204  uncfcurf  18205  diagval  18206  curf2ndf  18213  hofval  18218  hof2fval  18221  hofcl  18225  yonval  18227  hofpropd  18233  yonedalem21  18239  yonedalem22  18244  yonedalem3  18246  xpsmnd0  18746  xpsinv  19036  xpsgrpsub  19037  symg2bas  19368  xpsring1d  20313  funcrngcsetc  20617  funcrngcsetcALT  20618  funcringcsetc  20651  rngqiprngimfv  21296  rngqiprngghm  21297  rngqiprngimf1  21298  rngqiprngimfo  21299  rngqiprnglin  21300  rngqipring1  21314  rngqiprngfu  21315  pzriprnglem6  21466  pzriprnglem12  21472  mat1dimmul  22441  txcnp  23585  upxp  23588  uptx  23590  hauseqlcld  23611  txlm  23613  txkgen  23617  cnmpt1t  23630  cnmpt2t  23638  txhmeo  23768  flfcnp2  23972  ucnimalem  24244  ucnima  24245  fmucndlem  24255  fmucnd  24256  cnheiborlem  24921  pi1xfrcnvlem  25023  ovollb2lem  25455  ovollb2  25456  ovolshftlem2  25477  ovolscalem2  25481  ioombl1  25529  ioorf  25540  ioorval  25541  ioorinv2  25542  uniioombllem6  25555  dyadval  25559  opnmbl  25569  mbfimaopnlem  25622  limccnp2  25859  mpodvdsmulf1o  27157  dvdsmulf1o  27159  precsexlemcbv  28198  precsexlem3  28201  seqseq123d  28278  om2noseqrdg  28296  noseqrdgsuc  28300  ebtwntg  29051  numclwwlk1lem2fv  30426  numclwwlk1lem2fo  30428  numclwwlk1lem2  30430  wlkl0  30437  hhssnvt  31336  hhsssh  31340  opsbc2ie  32545  opreu2reuALT  32546  opfv  32717  xppreima  32718  2ndresdju  32722  aciunf1lem  32735  ofpreima  32738  fgreu  32744  gsumwrd2dccatlem  33138  gsumwrd2dccat  33139  rlocval  33320  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  zringfrac  33614  smatlem  33941  qtophaus  33980  qqhval2  34126  esum2dlem  34236  rrvadd  34596  hgt750lemb  34800  bnj1442  35191  bnj1450  35192  bnj1463  35197  bnj1529  35212  swrdrevpfx  35299  erdszelem9  35381  erdszelem10  35382  txpconn  35414  txsconnlem  35422  goaleq12d  35533  msubval  35707  msubco  35713  mvhval  35716  msubvrs  35742  cbvoprab123vw  36421  cbvoprab23vw  36422  cbvoprab13vw  36423  cbvopabdavw  36448  cbvoprab123davw  36456  cbvoprab12davw  36457  cbvoprab23davw  36458  cbvoprab13davw  36459  bj-dfid2ALT  37372  bj-endval  37629  finxpreclem3  37709  poimirlem4  37945  opnmbllem0  37977  mblfinlem1  37978  mblfinlem2  37979  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  nfopdALT  39417  dvhvaddcbv  41535  dvhvaddval  41536  dvhopvadd  41539  dvhvaddcomN  41542  dvhvaddass  41543  dvhvscacbv  41544  dvhvscaval  41545  dvhopvsca  41548  dvhgrp  41553  dvhlveclem  41554  dvh0g  41557  dvhopaddN  41560  dvhopspN  41561  dvhopN  41562  cdlemn4  41644  hdmapffval  42272  pellexlem3  43259  pellex  43263  elcnvlem  44028  dvnprodlem1  46374  dvnprodlem3  46376  etransclem44  46706  ovolval4  47079  ovolval5lem3  47082  aoveq123d  47620  prproropf1olem2  47958  prproropf1olem3  47959  prproropf1olem4  47960  prproropf1o  47961  prproropreud  47963  isisubgr  48332  eloprab1st2nd  49337  ssccatid  49541  oppfvalg  49595  imaf1co  49624  uptrlem1  49679  xpcfucco3  49727  dfswapf2  49730  swapfval  49731  swapfcoa  49750  1stfpropd  49759  2ndfpropd  49760  tposcurf1  49768  diag1  49773  fuco2eld2  49783  fucofvalg  49787  fuco21  49805  fuco11bALT  49807  fuco23  49810  fuco22natlem3  49813  fuco22nat  49815  fucoid  49817  fuco22a  49819  fucocolem2  49823  fucocolem4  49825  postcofval  49833  precofval  49836  precofvalALT  49837  precofval3  49840  prcofvalg  49845  prcofpropd  49848  prcofdiag1  49862  prcofdiag  49863  fucoppcco  49878  oppfdiag1  49883  oppfdiag  49885  termcfuncval  50001  diag1f1olem  50002  mndtcval  50048  mndtcco  50054  2arwcatlem2  50065  2arwcatlem3  50066  2arwcatlem4  50067  2arwcat  50069  setc1onsubc  50071  lanfval  50082  ranfval  50083  ranup  50111  concom  50132  islmd  50134