Theorem opeq12d 4832

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582

This theorem is referenced by:  nfopd  4841  moop2  5445  iunopeqop  5464  dfid2  5516  fsn2g  7077  funopsn  7087  fnprb  7148  fntpb  7149  fnpr2g  7150  fliftfuns  7254  dfmpo  8038  fsplit  8053  fsplitfpar  8054  fnwelem  8067  fimaproj  8071  seqomlem0  8374  seqomlem1  8375  seqomlem4  8378  qliftfuns  8734  xpassen  8991  xpdom2  8992  xpf1o  9059  xpmapenlem  9064  xpmapen  9065  mapunen  9066  xpwdomg  9478  fseqenlem2  9923  nqereu  10827  addpipq2  10834  addpipq  10835  mulpipq2  10837  mulpipq  10838  1nqenq  10860  mulidnq  10861  ltexnq  10873  prlem934  10931  addsrmo  10971  mulsrmo  10972  addsrpr  10973  mulsrpr  10974  mulcnsr  11034  mulresr  11037  axcnre  11062  om2uzrdg  13865  uzrdgsuci  13869  pfxsuff1eqwrdeq  14608  swrdpfx  14616  ccatopth  14625  swrdccatin2d  14653  splval  14660  splcl  14661  cshfn  14699  repswcshw  14721  2swrd2eqwrdeq  14862  ruclem1  16142  eucalgval2  16494  qnumdenbi  16657  crth  16691  phimullem  16692  prmreclem3  16832  setsstruct  17089  ressval3d  17159  imasval  17417  imasaddvallem  17435  xpsff1o  17473  catidex  17582  cidval  17585  catcocl  17593  catass  17594  oppccofval  17624  sectfval  17660  subccocl  17754  isfunc  17773  funcco  17780  idfuval  17785  idfucl  17790  cofuval  17791  cofuval2  17796  cofucl  17797  cofuass  17798  cofulid  17799  cofurid  17800  resfval  17801  resfval2  17802  funcres  17805  inclfusubc  17852  isnat  17859  nati  17867  fucco  17874  fuccoval  17875  coaval  17977  catcisolem  18019  xpcval  18085  xpcco  18091  xpcco2  18095  xpccatid  18096  xpcid  18097  1stfval  18099  2ndfval  18102  1stfcl  18105  2ndfcl  18106  prfval  18107  prf1  18108  prf2fval  18109  prf2  18110  prfcl  18111  prf1st  18112  prf2nd  18113  1st2ndprf  18114  xpcpropd  18116  evlfval  18125  evlf2  18126  evlfcllem  18129  evlfcl  18130  curfval  18131  curf1  18133  curf1cl  18136  curf2cl  18139  curfcl  18140  curfpropd  18141  uncf1  18144  uncf2  18145  curfuncf  18146  uncfcurf  18147  diagval  18148  curf2ndf  18155  hofval  18160  hof2fval  18163  hofcl  18167  yonval  18169  hofpropd  18175  yonedalem21  18181  yonedalem22  18186  yonedalem3  18188  xpsmnd0  18688  xpsinv  18975  xpsgrpsub  18976  symg2bas  19307  xpsring1d  20253  funcrngcsetc  20557  funcrngcsetcALT  20558  funcringcsetc  20591  rngqiprngimfv  21237  rngqiprngghm  21238  rngqiprngimf1  21239  rngqiprngimfo  21240  rngqiprnglin  21241  rngqipring1  21255  rngqiprngfu  21256  pzriprnglem6  21425  pzriprnglem12  21431  mat1dimmul  22392  txcnp  23536  upxp  23539  uptx  23541  hauseqlcld  23562  txlm  23564  txkgen  23568  cnmpt1t  23581  cnmpt2t  23589  txhmeo  23719  flfcnp2  23923  ucnimalem  24195  ucnima  24196  fmucndlem  24206  fmucnd  24207  cnheiborlem  24881  pi1xfrcnvlem  24984  ovollb2lem  25417  ovollb2  25418  ovolshftlem2  25439  ovolscalem2  25443  ioombl1  25491  ioorf  25502  ioorval  25503  ioorinv2  25504  uniioombllem6  25517  dyadval  25521  opnmbl  25531  mbfimaopnlem  25584  limccnp2  25821  mpodvdsmulf1o  27132  dvdsmulf1o  27134  precsexlemcbv  28145  precsexlem3  28148  seqseq123d  28217  om2noseqrdg  28235  noseqrdgsuc  28239  ebtwntg  28962  numclwwlk1lem2fv  30338  numclwwlk1lem2fo  30340  numclwwlk1lem2  30342  wlkl0  30349  hhssnvt  31247  hhsssh  31251  opsbc2ie  32457  opreu2reuALT  32458  opfv  32628  xppreima  32629  2ndresdju  32633  aciunf1lem  32646  ofpreima  32649  fgreu  32656  gsumwrd2dccatlem  33053  gsumwrd2dccat  33054  rlocval  33233  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rloc0g  33245  rloc1r  33246  rlocf1  33247  zringfrac  33526  smatlem  33831  qtophaus  33870  qqhval2  34016  esum2dlem  34126  rrvadd  34486  hgt750lemb  34690  bnj1442  35082  bnj1450  35083  bnj1463  35088  bnj1529  35103  swrdrevpfx  35182  erdszelem9  35264  erdszelem10  35265  txpconn  35297  txsconnlem  35305  goaleq12d  35416  msubval  35590  msubco  35596  mvhval  35599  msubvrs  35625  cbvoprab123vw  36304  cbvoprab23vw  36305  cbvoprab13vw  36306  cbvopabdavw  36331  cbvoprab123davw  36339  cbvoprab12davw  36340  cbvoprab23davw  36341  cbvoprab13davw  36342  bj-dfid2ALT  37130  bj-endval  37380  finxpreclem3  37458  poimirlem4  37685  opnmbllem0  37717  mblfinlem1  37718  mblfinlem2  37719  heiborlem6  37877  heiborlem7  37878  heiborlem8  37879  nfopdALT  39091  dvhvaddcbv  41209  dvhvaddval  41210  dvhopvadd  41213  dvhvaddcomN  41216  dvhvaddass  41217  dvhvscacbv  41218  dvhvscaval  41219  dvhopvsca  41222  dvhgrp  41227  dvhlveclem  41228  dvh0g  41231  dvhopaddN  41234  dvhopspN  41235  dvhopN  41236  cdlemn4  41318  hdmapffval  41946  pellexlem3  42949  pellex  42953  elcnvlem  43719  dvnprodlem1  46069  dvnprodlem3  46071  etransclem44  46401  ovolval4  46774  ovolval5lem3  46777  aoveq123d  47303  prproropf1olem2  47629  prproropf1olem3  47630  prproropf1olem4  47631  prproropf1o  47632  prproropreud  47634  isisubgr  47987  eloprab1st2nd  48993  ssccatid  49198  oppfvalg  49252  imaf1co  49281  uptrlem1  49336  xpcfucco3  49384  dfswapf2  49387  swapfval  49388  swapfcoa  49407  1stfpropd  49416  2ndfpropd  49417  tposcurf1  49425  diag1  49430  fuco2eld2  49440  fucofvalg  49444  fuco21  49462  fuco11bALT  49464  fuco23  49467  fuco22natlem3  49470  fuco22nat  49472  fucoid  49474  fuco22a  49476  fucocolem2  49480  fucocolem4  49482  postcofval  49490  precofval  49493  precofvalALT  49494  precofval3  49497  prcofvalg  49502  prcofpropd  49505  prcofdiag1  49519  prcofdiag  49520  fucoppcco  49535  oppfdiag1  49540  oppfdiag  49542  termcfuncval  49658  diag1f1olem  49659  mndtcval  49705  mndtcco  49711  2arwcatlem2  49722  2arwcatlem3  49723  2arwcatlem4  49724  2arwcat  49726  setc1onsubc  49728  lanfval  49739  ranfval  49740  ranup  49768  concom  49789  islmd  49791