Theorem opeq12d 4824

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  nfopd  4833  moop2  5456  iunopeqop  5475  iunopeqopOLD  5476  dfid2  5528  fsn2g  7091  funopsn  7101  funopsnOLD  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  47626  prproropf1olem2  47964  prproropf1olem3  47965  prproropf1olem4  47966  prproropf1o  47967  prproropreud  47969  isisubgr  48338  eloprab1st2nd  49343  ssccatid  49547  oppfvalg  49601  imaf1co  49630  uptrlem1  49685  xpcfucco3  49733  dfswapf2  49736  swapfval  49737  swapfcoa  49756  1stfpropd  49765  2ndfpropd  49766  tposcurf1  49774  diag1  49779  fuco2eld2  49789  fucofvalg  49793  fuco21  49811  fuco11bALT  49813  fuco23  49816  fuco22natlem3  49819  fuco22nat  49821  fucoid  49823  fuco22a  49825  fucocolem2  49829  fucocolem4  49831  postcofval  49839  precofval  49842  precofvalALT  49843  precofval3  49846  prcofvalg  49851  prcofpropd  49854  prcofdiag1  49868  prcofdiag  49869  fucoppcco  49884  oppfdiag1  49889  oppfdiag  49891  termcfuncval  50007  diag1f1olem  50008  mndtcval  50054  mndtcco  50060  2arwcatlem2  50071  2arwcatlem3  50072  2arwcatlem4  50073  2arwcat  50075  setc1onsubc  50077  lanfval  50088  ranfval  50089  ranup  50117  concom  50138  islmd  50140