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  5450  iunopeqop  5469  dfid2  5521  fsn2g  7085  funopsn  7095  fnprb  7156  fntpb  7157  fnpr2g  7158  fliftfuns  7262  dfmpo  8045  fsplit  8060  fsplitfpar  8061  fnwelem  8074  fimaproj  8078  seqomlem0  8381  seqomlem1  8382  seqomlem4  8385  qliftfuns  8744  xpassen  9002  xpdom2  9003  xpf1o  9070  xpmapenlem  9075  xpmapen  9076  mapunen  9077  xpwdomg  9493  fseqenlem2  9938  nqereu  10843  addpipq2  10850  addpipq  10851  mulpipq2  10853  mulpipq  10854  1nqenq  10876  mulidnq  10877  ltexnq  10889  prlem934  10947  addsrmo  10987  mulsrmo  10988  addsrpr  10989  mulsrpr  10990  mulcnsr  11050  mulresr  11053  axcnre  11078  om2uzrdg  13909  uzrdgsuci  13913  pfxsuff1eqwrdeq  14652  swrdpfx  14660  ccatopth  14669  swrdccatin2d  14697  splval  14704  splcl  14705  cshfn  14743  repswcshw  14765  2swrd2eqwrdeq  14906  ruclem1  16189  eucalgval2  16541  qnumdenbi  16705  crth  16739  phimullem  16740  prmreclem3  16880  setsstruct  17137  ressval3d  17207  imasval  17466  imasaddvallem  17484  xpsff1o  17522  catidex  17631  cidval  17634  catcocl  17642  catass  17643  oppccofval  17673  sectfval  17709  subccocl  17803  isfunc  17822  funcco  17829  idfuval  17834  idfucl  17839  cofuval  17840  cofuval2  17845  cofucl  17846  cofuass  17847  cofulid  17848  cofurid  17849  resfval  17850  resfval2  17851  funcres  17854  inclfusubc  17901  isnat  17908  nati  17916  fucco  17923  fuccoval  17924  coaval  18026  catcisolem  18068  xpcval  18134  xpcco  18140  xpcco2  18144  xpccatid  18145  xpcid  18146  1stfval  18148  2ndfval  18151  1stfcl  18154  2ndfcl  18155  prfval  18156  prf1  18157  prf2fval  18158  prf2  18159  prfcl  18160  prf1st  18161  prf2nd  18162  1st2ndprf  18163  xpcpropd  18165  evlfval  18174  evlf2  18175  evlfcllem  18178  evlfcl  18179  curfval  18180  curf1  18182  curf1cl  18185  curf2cl  18188  curfcl  18189  curfpropd  18190  uncf1  18193  uncf2  18194  curfuncf  18195  uncfcurf  18196  diagval  18197  curf2ndf  18204  hofval  18209  hof2fval  18212  hofcl  18216  yonval  18218  hofpropd  18224  yonedalem21  18230  yonedalem22  18235  yonedalem3  18237  xpsmnd0  18737  xpsinv  19027  xpsgrpsub  19028  symg2bas  19359  xpsring1d  20304  funcrngcsetc  20608  funcrngcsetcALT  20609  funcringcsetc  20642  rngqiprngimfv  21288  rngqiprngghm  21289  rngqiprngimf1  21290  rngqiprngimfo  21291  rngqiprnglin  21292  rngqipring1  21306  rngqiprngfu  21307  pzriprnglem6  21476  pzriprnglem12  21482  mat1dimmul  22451  txcnp  23595  upxp  23598  uptx  23600  hauseqlcld  23621  txlm  23623  txkgen  23627  cnmpt1t  23640  cnmpt2t  23648  txhmeo  23778  flfcnp2  23982  ucnimalem  24254  ucnima  24255  fmucndlem  24265  fmucnd  24266  cnheiborlem  24931  pi1xfrcnvlem  25033  ovollb2lem  25465  ovollb2  25466  ovolshftlem2  25487  ovolscalem2  25491  ioombl1  25539  ioorf  25550  ioorval  25551  ioorinv2  25552  uniioombllem6  25565  dyadval  25569  opnmbl  25579  mbfimaopnlem  25632  limccnp2  25869  mpodvdsmulf1o  27171  dvdsmulf1o  27173  precsexlemcbv  28212  precsexlem3  28215  seqseq123d  28292  om2noseqrdg  28310  noseqrdgsuc  28314  ebtwntg  29065  numclwwlk1lem2fv  30441  numclwwlk1lem2fo  30443  numclwwlk1lem2  30445  wlkl0  30452  hhssnvt  31351  hhsssh  31355  opsbc2ie  32560  opreu2reuALT  32561  opfv  32732  xppreima  32733  2ndresdju  32737  aciunf1lem  32750  ofpreima  32753  fgreu  32759  gsumwrd2dccatlem  33153  gsumwrd2dccat  33154  rlocval  33335  rlocaddval  33344  rlocmulval  33345  rloccring  33346  rloc0g  33347  rloc1r  33348  rlocf1  33349  zringfrac  33629  smatlem  33957  qtophaus  33996  qqhval2  34142  esum2dlem  34252  rrvadd  34612  hgt750lemb  34816  bnj1442  35207  bnj1450  35208  bnj1463  35213  bnj1529  35228  swrdrevpfx  35315  erdszelem9  35397  erdszelem10  35398  txpconn  35430  txsconnlem  35438  goaleq12d  35549  msubval  35723  msubco  35729  mvhval  35732  msubvrs  35758  cbvoprab123vw  36437  cbvoprab23vw  36438  cbvoprab13vw  36439  cbvopabdavw  36464  cbvoprab123davw  36472  cbvoprab12davw  36473  cbvoprab23davw  36474  cbvoprab13davw  36475  bj-dfid2ALT  37388  bj-endval  37645  finxpreclem3  37723  poimirlem4  37959  opnmbllem0  37991  mblfinlem1  37992  mblfinlem2  37993  heiborlem6  38151  heiborlem7  38152  heiborlem8  38153  nfopdALT  39431  dvhvaddcbv  41549  dvhvaddval  41550  dvhopvadd  41553  dvhvaddcomN  41556  dvhvaddass  41557  dvhvscacbv  41558  dvhvscaval  41559  dvhopvsca  41562  dvhgrp  41567  dvhlveclem  41568  dvh0g  41571  dvhopaddN  41574  dvhopspN  41575  dvhopN  41576  cdlemn4  41658  hdmapffval  42286  pellexlem3  43277  pellex  43281  elcnvlem  44046  dvnprodlem1  46392  dvnprodlem3  46394  etransclem44  46724  ovolval4  47097  ovolval5lem3  47100  aoveq123d  47638  prproropf1olem2  47976  prproropf1olem3  47977  prproropf1olem4  47978  prproropf1o  47979  prproropreud  47981  isisubgr  48350  eloprab1st2nd  49355  ssccatid  49559  oppfvalg  49613  imaf1co  49642  uptrlem1  49697  xpcfucco3  49745  dfswapf2  49748  swapfval  49749  swapfcoa  49768  1stfpropd  49777  2ndfpropd  49778  tposcurf1  49786  diag1  49791  fuco2eld2  49801  fucofvalg  49805  fuco21  49823  fuco11bALT  49825  fuco23  49828  fuco22natlem3  49831  fuco22nat  49833  fucoid  49835  fuco22a  49837  fucocolem2  49841  fucocolem4  49843  postcofval  49851  precofval  49854  precofvalALT  49855  precofval3  49858  prcofvalg  49863  prcofpropd  49866  prcofdiag1  49880  prcofdiag  49881  fucoppcco  49896  oppfdiag1  49901  oppfdiag  49903  termcfuncval  50019  diag1f1olem  50020  mndtcval  50066  mndtcco  50072  2arwcatlem2  50083  2arwcatlem3  50084  2arwcatlem4  50085  2arwcat  50087  setc1onsubc  50089  lanfval  50100  ranfval  50101  ranup  50129  concom  50150  islmd  50152