Theorem opeq12d 4838

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

Syntax hints:   → wi 4   = wceq 1559  ⟨cop 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588

This theorem is referenced by:  nfopd  4847  moop2  5470  iunopeqop  5489  iunopeqopOLD  5490  dfid2  5542  fsn2g  7116  funopsn  7126  funopsnOLD  7127  fnprb  7188  fntpb  7189  fnpr2g  7190  fliftfuns  7294  dfmpo  8076  fsplit  8091  fsplitfpar  8092  fnwelem  8106  fimaproj  8110  seqomlem0  8415  seqomlem1  8416  seqomlem4  8419  qliftfuns  8781  xpassen  9039  xpdom2  9040  xpf1o  9107  xpmapenlem  9112  xpmapen  9113  mapunen  9114  xpwdomg  9530  fseqenlem2  9978  nqereu  10884  addpipq2  10891  addpipq  10892  mulpipq2  10894  mulpipq  10895  1nqenq  10917  mulidnq  10918  ltexnq  10930  prlem934  10988  addsrmo  11028  mulsrmo  11029  addsrpr  11030  mulsrpr  11031  mulcnsr  11091  mulresr  11094  axcnre  11119  om2uzrdg  13966  uzrdgsuci  13970  pfxsuff1eqwrdeq  14709  swrdpfx  14717  ccatopth  14726  swrdccatin2d  14754  splval  14761  splcl  14762  cshfn  14800  repswcshw  14822  2swrd2eqwrdeq  14963  ruclem1  16246  eucalgval2  16598  qnumdenbi  16762  crth  16796  phimullem  16797  prmreclem3  16937  setsstruct  17195  ressval3d  17265  imasval  17524  imasaddvallem  17542  xpsff1o  17580  catidex  17689  cidval  17692  catcocl  17700  catass  17701  oppccofval  17731  sectfval  17767  subccocl  17861  isfunc  17880  funcco  17887  idfuval  17892  idfucl  17897  cofuval  17898  cofuval2  17903  cofucl  17904  cofuass  17905  cofulid  17906  cofurid  17907  resfval  17908  resfval2  17909  funcres  17912  inclfusubc  17959  isnat  17966  nati  17974  fucco  17981  fuccoval  17982  coaval  18084  catcisolem  18126  xpcval  18192  xpcco  18198  xpcco2  18202  xpccatid  18203  xpcid  18204  1stfval  18206  2ndfval  18209  1stfcl  18212  2ndfcl  18213  prfval  18214  prf1  18215  prf2fval  18216  prf2  18217  prfcl  18218  prf1st  18219  prf2nd  18220  1st2ndprf  18221  xpcpropd  18223  evlfval  18232  evlf2  18233  evlfcllem  18236  evlfcl  18237  curfval  18238  curf1  18240  curf1cl  18243  curf2cl  18246  curfcl  18247  curfpropd  18248  uncf1  18251  uncf2  18252  curfuncf  18253  uncfcurf  18254  diagval  18255  curf2ndf  18262  hofval  18267  hof2fval  18270  hofcl  18274  yonval  18276  hofpropd  18282  yonedalem21  18288  yonedalem22  18293  yonedalem3  18295  xpsmnd0  18795  xpsinv  19085  xpsgrpsub  19086  symg2bas  19416  xpsring1d  20361  funcrngcsetc  20669  funcrngcsetcALT  20670  funcringcsetc  20703  rngqiprngimfv  21348  rngqiprngghm  21349  rngqiprngimf1  21350  rngqiprngimfo  21351  rngqiprnglin  21352  rngqipring1  21366  rngqiprngfu  21367  pzriprnglem6  21518  pzriprnglem12  21524  mat1dimmul  22516  txcnp  23660  upxp  23663  uptx  23665  hauseqlcld  23686  txlm  23688  txkgen  23692  cnmpt1t  23705  cnmpt2t  23713  txhmeo  23843  flfcnp2  24047  ucnimalem  24319  ucnima  24320  fmucndlem  24330  fmucnd  24331  cnheiborlem  24996  pi1xfrcnvlem  25098  ovollb2lem  25530  ovollb2  25531  ovolshftlem2  25552  ovolscalem2  25556  ioombl1  25604  ioorf  25615  ioorval  25616  ioorinv2  25617  uniioombllem6  25630  dyadval  25634  opnmbl  25644  mbfimaopnlem  25697  limccnp2  25934  mpodvdsmulf1o  27235  dvdsmulf1o  27237  precsexlemcbv  28276  precsexlem3  28279  seqseq123d  28356  om2noseqrdg  28374  noseqrdgsuc  28378  ebtwntg  29129  numclwwlk1lem2fv  30504  numclwwlk1lem2fo  30506  numclwwlk1lem2  30508  wlkl0  30515  hhssnvt  31414  hhsssh  31418  opsbc2ie  32623  opreu2reuALT  32624  opfv  32796  xppreima  32797  2ndresdju  32801  aciunf1lem  32814  ofpreima  32817  fgreu  32823  gsumwrd2dccatlem  33218  gsumwrd2dccat  33219  rlocval  33401  rlocaddval  33411  rlocmulval  33412  rloccring  33413  rloc0g  33414  rloc1r  33415  rlocf1  33416  rlocinvunit  33417  rlocisunit  33418  zringfrac  33711  smatlem  34055  qtophaus  34094  qqhval2  34240  esum2dlem  34350  rrvadd  34710  hgt750lemb  34914  bnj1442  35308  bnj1450  35309  bnj1463  35314  bnj1529  35329  swrdrevpfx  35431  erdszelem9  35513  erdszelem10  35514  txpconn  35546  txsconnlem  35554  goaleq12d  35665  msubval  35839  msubco  35845  mvhval  35848  msubvrs  35874  cbvoprab123vw  36563  cbvoprab23vw  36564  cbvoprab13vw  36565  cbvopabdavw  36590  cbvoprab123davw  36598  cbvoprab12davw  36599  cbvoprab23davw  36600  cbvoprab13davw  36601  bj-dfid2ALT  37514  bj-endval  37771  finxpreclem3  37851  poimirlem4  38087  opnmbllem0  38119  mblfinlem1  38120  mblfinlem2  38121  heiborlem6  38279  heiborlem7  38280  heiborlem8  38281  nfopdALT  39559  dvhvaddcbv  41677  dvhvaddval  41678  dvhopvadd  41681  dvhvaddcomN  41684  dvhvaddass  41685  dvhvscacbv  41686  dvhvscaval  41687  dvhopvsca  41690  dvhgrp  41695  dvhlveclem  41696  dvh0g  41699  dvhopaddN  41702  dvhopspN  41703  dvhopN  41704  cdlemn4  41786  hdmapffval  42414  pellexlem3  43372  pellex  43376  elcnvlem  44141  dvnprodlem1  46484  dvnprodlem3  46486  etransclem44  46816  ovolval4  47189  ovolval5lem3  47192  aoveq123d  47736  prproropf1olem2  48074  prproropf1olem3  48075  prproropf1olem4  48076  prproropf1o  48077  prproropreud  48079  isisubgr  48448  eloprab1st2nd  49453  ssccatid  49657  oppfvalg  49711  imaf1co  49740  uptrlem1  49795  xpcfucco3  49843  dfswapf2  49846  swapfval  49847  swapfcoa  49866  1stfpropd  49875  2ndfpropd  49876  tposcurf1  49884  diag1  49889  fuco2eld2  49899  fucofvalg  49903  fuco21  49921  fuco11bALT  49923  fuco23  49926  fuco22natlem3  49929  fuco22nat  49931  fucoid  49933  fuco22a  49935  fucocolem2  49939  fucocolem4  49941  postcofval  49949  precofval  49952  precofvalALT  49953  precofval3  49956  prcofvalg  49961  prcofpropd  49964  prcofdiag1  49978  prcofdiag  49979  fucoppcco  49994  oppfdiag1  49999  oppfdiag  50001  termcfuncval  50117  diag1f1olem  50118  mndtcval  50164  mndtcco  50170  2arwcatlem2  50181  2arwcatlem3  50182  2arwcatlem4  50183  2arwcat  50185  setc1onsubc  50187  lanfval  50198  ranfval  50199  ranup  50227  concom  50248  islmd  50250