Theorem opeq12d 4847

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

Syntax hints:   → wi 4   = wceq 1570  ⟨cop 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597

This theorem is referenced by:  nfopd  4856  moop2  5487  iunopeqop  5506  iunopeqopOLD  5507  dfid2  5560  fsn2g  7136  funopsn  7146  funopsnOLD  7147  fnprb  7208  fntpb  7209  fnpr2g  7210  fliftfuns  7314  dfmpo  8098  fsplit  8113  fsplitfpar  8114  fnwelem  8128  fimaproj  8132  seqomlem0  8437  seqomlem1  8438  seqomlem4  8441  qliftfuns  8803  xpassen  9060  xpdom2  9061  xpf1o  9128  xpmapenlem  9133  xpmapen  9134  mapunen  9135  xpwdomg  9548  fseqenlem2  10010  nqereu  10915  addpipq2  10922  addpipq  10923  mulpipq2  10925  mulpipq  10926  1nqenq  10948  mulidnq  10949  ltexnq  10961  prlem934  11019  addsrmo  11059  mulsrmo  11060  addsrpr  11061  mulsrpr  11062  mulcnsr  11122  mulresr  11125  axcnre  11150  om2uzrdg  13994  uzrdgsuci  13998  pfxsuff1eqwrdeq  14738  swrdpfx  14746  ccatopth  14755  swrdccatin2d  14783  splval  14790  splcl  14791  cshfn  14829  repswcshw  14851  2swrd2eqwrdeq  14992  ruclem1  16288  eucalgval2  16640  qnumdenbi  16804  crth  16838  phimullem  16839  prmreclem3  16979  setsstruct  17237  ressval3d  17307  imasval  17566  imasaddvallem  17584  xpsff1o  17622  catidex  17731  cidval  17734  catcocl  17742  catass  17743  oppccofval  17773  sectfval  17809  subccocl  17903  isfunc  17922  funcco  17929  idfuval  17934  idfucl  17939  cofuval  17940  cofuval2  17945  cofucl  17946  cofuass  17947  cofulid  17948  cofurid  17949  resfval  17950  resfval2  17951  funcres  17954  inclfusubc  18001  isnat  18008  nati  18016  fucco  18023  fuccoval  18024  coaval  18126  catcisolem  18168  xpcval  18234  xpcco  18240  xpcco2  18244  xpccatid  18245  xpcid  18246  1stfval  18248  2ndfval  18251  1stfcl  18254  2ndfcl  18255  prfval  18256  prf1  18257  prf2fval  18258  prf2  18259  prfcl  18260  prf1st  18261  prf2nd  18262  1st2ndprf  18263  xpcpropd  18265  evlfval  18274  evlf2  18275  evlfcllem  18278  evlfcl  18279  curfval  18280  curf1  18282  curf1cl  18285  curf2cl  18288  curfcl  18289  curfpropd  18290  uncf1  18293  uncf2  18294  curfuncf  18295  uncfcurf  18296  diagval  18297  curf2ndf  18304  hofval  18309  hof2fval  18312  hofcl  18316  yonval  18318  hofpropd  18324  yonedalem21  18330  yonedalem22  18335  yonedalem3  18337  xpsmnd0  18837  xpsinv  19127  xpsgrpsub  19128  symg2bas  19464  xpsring1d  20416  funcrngcsetc  20726  funcrngcsetcALT  20727  funcringcsetc  20760  rngqiprngimfv  21419  rngqiprngghm  21420  rngqiprngimf1  21421  rngqiprngimfo  21422  rngqiprnglin  21423  rngqipring1  21437  rngqiprngfu  21438  pzriprnglem6  21617  pzriprnglem12  21623  mat1dimmul  22614  txcnp  23758  upxp  23761  uptx  23763  hauseqlcld  23784  txlm  23786  txkgen  23790  cnmpt1t  23803  cnmpt2t  23811  txhmeo  23941  flfcnp2  24145  ucnimalem  24417  ucnima  24418  fmucndlem  24428  fmucnd  24429  cnheiborlem  25094  pi1xfrcnvlem  25196  ovollb2lem  25628  ovollb2  25629  ovolshftlem2  25650  ovolscalem2  25654  ioombl1  25702  ioorf  25713  ioorval  25714  ioorinv2  25715  uniioombllem6  25728  dyadval  25732  opnmbl  25742  mbfimaopnlem  25795  limccnp2  26032  mpodvdsmulf1o  27339  dvdsmulf1o  27341  precsexlemcbv  28380  precsexlem3  28383  seqseq123d  28460  om2noseqrdg  28478  noseqrdgsuc  28482  ebtwntg  29313  numclwwlk1lem2fv  30688  numclwwlk1lem2fo  30690  numclwwlk1lem2  30692  wlkl0  30699  hhssnvt  31598  hhsssh  31602  opsbc2ie  32803  opreu2reuALT  32804  opfv  32970  xppreima  32971  2ndresdju  32975  aciunf1lem  32988  ofpreima  32991  fgreu  32997  gsumwrd2dccatlem  33378  gsumwrd2dccat  33379  rlocval  33560  rlocaddval  33570  rlocmulval  33571  rloccring  33572  rloc0g  33573  rloc1r  33574  rlocf1  33575  rlocinvunit  33576  rlocisunit  33577  zringfrac  33825  smatlem  34168  qtophaus  34207  qqhval2  34353  esum2dlem  34463  rrvadd  34823  hgt750lemb  35024  bnj1442  35418  bnj1450  35419  bnj1463  35424  bnj1529  35439  swrdrevpfx  35589  erdszelem9  35672  erdszelem10  35673  txpconn  35705  txsconnlem  35713  goaleq12d  35824  msubval  35998  msubco  36004  mvhval  36007  msubvrs  36033  cbvoprab123vw  36732  cbvoprab23vw  36733  cbvoprab13vw  36734  cbvopabdavw  36759  cbvoprab123davw  36767  cbvoprab12davw  36768  cbvoprab23davw  36769  cbvoprab13davw  36770  bj-dfid2ALT  37682  bj-endval  37940  finxpreclem3  38020  poimirlem4  38256  opnmbllem0  38288  mblfinlem1  38289  mblfinlem2  38290  heiborlem6  38448  heiborlem7  38449  heiborlem8  38450  nfopdALT  39726  dvhvaddcbv  41844  dvhvaddval  41845  dvhopvadd  41848  dvhvaddcomN  41851  dvhvaddass  41852  dvhvscacbv  41853  dvhvscaval  41854  dvhopvsca  41857  dvhgrp  41862  dvhlveclem  41863  dvh0g  41866  dvhopaddN  41869  dvhopspN  41870  dvhopN  41871  cdlemn4  41953  hdmapffval  42581  pellexlem3  43541  pellex  43545  elcnvlem  44310  dvnprodlem1  46643  dvnprodlem3  46645  etransclem44  46975  ovolval4  47348  ovolval5lem3  47351  aoveq123d  47898  prproropf1olem2  48236  prproropf1olem3  48237  prproropf1olem4  48238  prproropf1o  48239  prproropreud  48241  isisubgr  48610  eloprab1st2nd  49629  ssccatid  49833  oppfvalg  49887  imaf1co  49916  uptrlem1  49971  xpcfucco3  50019  dfswapf2  50022  swapfval  50023  swapfcoa  50042  1stfpropd  50051  2ndfpropd  50052  tposcurf1  50060  diag1  50065  fuco2eld2  50075  fucofvalg  50079  fuco21  50097  fuco11bALT  50099  fuco23  50102  fuco22natlem3  50105  fuco22nat  50107  fucoid  50109  fuco22a  50111  fucocolem2  50115  fucocolem4  50117  postcofval  50125  precofval  50128  precofvalALT  50129  precofval3  50132  prcofvalg  50137  prcofpropd  50140  prcofdiag1  50154  prcofdiag  50155  fucoppcco  50170  oppfdiag1  50175  oppfdiag  50177  termcfuncval  50293  diag1f1olem  50294  mndtcval  50340  mndtcco  50346  2arwcatlem2  50357  2arwcatlem3  50358  2arwcatlem4  50359  2arwcat  50361  setc1onsubc  50363  lanfval  50374  ranfval  50375  ranup  50403  concom  50424  islmd  50426