Theorem opeq12d 4833

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583

This theorem is referenced by:  nfopd  4842  moop2  5442  iunopeqop  5461  dfid2  5513  fsn2g  7071  funopsn  7081  fnprb  7142  fntpb  7143  fnpr2g  7144  fliftfuns  7248  dfmpo  8032  fsplit  8047  fsplitfpar  8048  fnwelem  8061  fimaproj  8065  seqomlem0  8368  seqomlem1  8369  seqomlem4  8372  qliftfuns  8728  xpassen  8984  xpdom2  8985  xpf1o  9052  xpmapenlem  9057  xpmapen  9058  mapunen  9059  xpwdomg  9471  fseqenlem2  9913  nqereu  10817  addpipq2  10824  addpipq  10825  mulpipq2  10827  mulpipq  10828  1nqenq  10850  mulidnq  10851  ltexnq  10863  prlem934  10921  addsrmo  10961  mulsrmo  10962  addsrpr  10963  mulsrpr  10964  mulcnsr  11024  mulresr  11027  axcnre  11052  om2uzrdg  13860  uzrdgsuci  13864  pfxsuff1eqwrdeq  14603  swrdpfx  14611  ccatopth  14620  swrdccatin2d  14648  splval  14655  splcl  14656  cshfn  14694  repswcshw  14716  2swrd2eqwrdeq  14857  ruclem1  16137  eucalgval2  16489  qnumdenbi  16652  crth  16686  phimullem  16687  prmreclem3  16827  setsstruct  17084  ressval3d  17154  imasval  17412  imasaddvallem  17430  xpsff1o  17468  catidex  17577  cidval  17580  catcocl  17588  catass  17589  oppccofval  17619  sectfval  17655  subccocl  17749  isfunc  17768  funcco  17775  idfuval  17780  idfucl  17785  cofuval  17786  cofuval2  17791  cofucl  17792  cofuass  17793  cofulid  17794  cofurid  17795  resfval  17796  resfval2  17797  funcres  17800  inclfusubc  17847  isnat  17854  nati  17862  fucco  17869  fuccoval  17870  coaval  17972  catcisolem  18014  xpcval  18080  xpcco  18086  xpcco2  18090  xpccatid  18091  xpcid  18092  1stfval  18094  2ndfval  18097  1stfcl  18100  2ndfcl  18101  prfval  18102  prf1  18103  prf2fval  18104  prf2  18105  prfcl  18106  prf1st  18107  prf2nd  18108  1st2ndprf  18109  xpcpropd  18111  evlfval  18120  evlf2  18121  evlfcllem  18124  evlfcl  18125  curfval  18126  curf1  18128  curf1cl  18131  curf2cl  18134  curfcl  18135  curfpropd  18136  uncf1  18139  uncf2  18140  curfuncf  18141  uncfcurf  18142  diagval  18143  curf2ndf  18150  hofval  18155  hof2fval  18158  hofcl  18162  yonval  18164  hofpropd  18170  yonedalem21  18176  yonedalem22  18181  yonedalem3  18183  xpsmnd0  18683  xpsinv  18970  xpsgrpsub  18971  symg2bas  19303  xpsring1d  20249  funcrngcsetc  20553  funcrngcsetcALT  20554  funcringcsetc  20587  rngqiprngimfv  21233  rngqiprngghm  21234  rngqiprngimf1  21235  rngqiprngimfo  21236  rngqiprnglin  21237  rngqipring1  21251  rngqiprngfu  21252  pzriprnglem6  21421  pzriprnglem12  21427  mat1dimmul  22389  txcnp  23533  upxp  23536  uptx  23538  hauseqlcld  23559  txlm  23561  txkgen  23565  cnmpt1t  23578  cnmpt2t  23586  txhmeo  23716  flfcnp2  23920  ucnimalem  24192  ucnima  24193  fmucndlem  24203  fmucnd  24204  cnheiborlem  24878  pi1xfrcnvlem  24981  ovollb2lem  25414  ovollb2  25415  ovolshftlem2  25436  ovolscalem2  25440  ioombl1  25488  ioorf  25499  ioorval  25500  ioorinv2  25501  uniioombllem6  25514  dyadval  25518  opnmbl  25528  mbfimaopnlem  25581  limccnp2  25818  mpodvdsmulf1o  27129  dvdsmulf1o  27131  precsexlemcbv  28142  precsexlem3  28145  seqseq123d  28214  om2noseqrdg  28232  noseqrdgsuc  28236  ebtwntg  28958  numclwwlk1lem2fv  30331  numclwwlk1lem2fo  30333  numclwwlk1lem2  30335  wlkl0  30342  hhssnvt  31240  hhsssh  31244  opsbc2ie  32450  opreu2reuALT  32451  opfv  32621  xppreima  32622  2ndresdju  32626  aciunf1lem  32639  ofpreima  32642  fgreu  32649  gsumwrd2dccatlem  33041  gsumwrd2dccat  33042  rlocval  33221  rlocaddval  33230  rlocmulval  33231  rloccring  33232  rloc0g  33233  rloc1r  33234  rlocf1  33235  zringfrac  33514  smatlem  33805  qtophaus  33844  qqhval2  33990  esum2dlem  34100  rrvadd  34460  hgt750lemb  34664  bnj1442  35056  bnj1450  35057  bnj1463  35062  bnj1529  35077  swrdrevpfx  35149  erdszelem9  35231  erdszelem10  35232  txpconn  35264  txsconnlem  35272  goaleq12d  35383  msubval  35557  msubco  35563  mvhval  35566  msubvrs  35592  cbvoprab123vw  36272  cbvoprab23vw  36273  cbvoprab13vw  36274  cbvopabdavw  36299  cbvoprab123davw  36307  cbvoprab12davw  36308  cbvoprab23davw  36309  cbvoprab13davw  36310  bj-dfid2ALT  37098  bj-endval  37348  finxpreclem3  37426  poimirlem4  37663  opnmbllem0  37695  mblfinlem1  37696  mblfinlem2  37697  heiborlem6  37855  heiborlem7  37856  heiborlem8  37857  nfopdALT  39009  dvhvaddcbv  41127  dvhvaddval  41128  dvhopvadd  41131  dvhvaddcomN  41134  dvhvaddass  41135  dvhvscacbv  41136  dvhvscaval  41137  dvhopvsca  41140  dvhgrp  41145  dvhlveclem  41146  dvh0g  41149  dvhopaddN  41152  dvhopspN  41153  dvhopN  41154  cdlemn4  41236  hdmapffval  41864  pellexlem3  42863  pellex  42867  elcnvlem  43633  dvnprodlem1  45983  dvnprodlem3  45985  etransclem44  46315  ovolval4  46688  ovolval5lem3  46691  aoveq123d  47208  prproropf1olem2  47534  prproropf1olem3  47535  prproropf1olem4  47536  prproropf1o  47537  prproropreud  47539  isisubgr  47892  eloprab1st2nd  48898  ssccatid  49103  oppfvalg  49157  imaf1co  49186  uptrlem1  49241  xpcfucco3  49289  dfswapf2  49292  swapfval  49293  swapfcoa  49312  1stfpropd  49321  2ndfpropd  49322  tposcurf1  49330  diag1  49335  fuco2eld2  49345  fucofvalg  49349  fuco21  49367  fuco11bALT  49369  fuco23  49372  fuco22natlem3  49375  fuco22nat  49377  fucoid  49379  fuco22a  49381  fucocolem2  49385  fucocolem4  49387  postcofval  49395  precofval  49398  precofvalALT  49399  precofval3  49402  prcofvalg  49407  prcofpropd  49410  prcofdiag1  49424  prcofdiag  49425  fucoppcco  49440  oppfdiag1  49445  oppfdiag  49447  termcfuncval  49563  diag1f1olem  49564  mndtcval  49610  mndtcco  49616  2arwcatlem2  49627  2arwcatlem3  49628  2arwcatlem4  49629  2arwcat  49631  setc1onsubc  49633  lanfval  49644  ranfval  49645  ranup  49673  concom  49694  islmd  49696