Theorem opeq12d 4851

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4838

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839

This theorem is used by:  nfopd  4853  moop2  5479  iunopeqop  5499  iunopeqopOLD  5500  dfid2  5553  fsn2g  7166  funopsn  7178  funopsnOLD  7179  fnprb  7240  fntpb  7241  fnpr2g  7242  fliftfuns  7348  dfmpo  8143  fsplit  8158  fsplitfpar  8159  fnwelem  8173  fimaproj  8182  seqomlem0  8490  seqomlem1  8491  seqomlem4  8494  qliftfuns  8856  xpassen  9121  xpdom2  9122  xpf1o  9189  xpmapenlem  9194  xpmapen  9195  mapunen  9196  xpwdomg  9609  fseqenlem2  10134  nqereu  11044  addpipq2  11051  addpipq  11052  mulpipq2  11054  mulpipq  11055  1nqenq  11077  mulidnq  11078  ltexnq  11090  prlem934  11148  addsrmo  11188  mulsrmo  11189  addsrpr  11190  mulsrpr  11191  mulcnsr  11251  mulresr  11254  axcnre  11279  om2uzrdg  14129  uzrdgsuci  14133  pfxsuff1eqwrdeq  14879  swrdpfx  14887  ccatopth  14896  swrdccatin2d  14924  splval  14931  splcl  14932  swrdrevpfx  14949  cshfn  14972  repswcshw  14994  2swrd2eqwrdeq  15138  ruclem1  16431  eucalgval2  16788  qnumdenbi  16952  crth  16987  phimullem  16988  prmreclem3  17128  setsstruct  17386  ressval3d  17456  imasval  17715  imasaddvallem  17733  xpsff1o  17771  catidex  17880  cidval  17883  catcocl  17891  catass  17892  oppccofval  17922  sectfval  17958  subccocl  18052  isfunc  18071  funcco  18078  idfuval  18083  idfucl  18088  cofuval  18089  cofuval2  18094  cofucl  18095  cofuass  18096  cofulid  18097  cofurid  18098  resfval  18099  resfval2  18100  funcres  18103  inclfusubc  18150  isnat  18157  nati  18165  fucco  18172  fuccoval  18173  coaval  18275  catcisolem  18317  xpcval  18383  xpcco  18389  xpcco2  18393  xpccatid  18394  xpcid  18395  1stfval  18397  2ndfval  18400  1stfcl  18403  2ndfcl  18404  prfval  18405  prf1  18406  prf2fval  18407  prf2  18408  prfcl  18409  prf1st  18410  prf2nd  18411  1st2ndprf  18412  xpcpropd  18414  evlfval  18423  evlf2  18424  evlfcllem  18427  evlfcl  18428  curfval  18429  curf1  18431  curf1cl  18434  curf2cl  18437  curfcl  18438  curfpropd  18439  uncf1  18442  uncf2  18443  curfuncf  18444  uncfcurf  18445  diagval  18446  curf2ndf  18453  hofval  18458  hof2fval  18461  hofcl  18465  yonval  18467  hofpropd  18473  yonedalem21  18479  yonedalem22  18484  yonedalem3  18486  xpsmnd0  19004  xpsinv  19302  xpsgrpsub  19303  symg2bas  19640  xpsring1d  20596  funcrngcsetc  20925  funcrngcsetcALT  20926  funcringcsetc  20959  rngqiprngimfv  21627  rngqiprngghm  21628  rngqiprngimf1  21629  rngqiprngimfo  21630  rngqiprnglin  21631  rngqipring1  21645  rngqiprngfu  21646  pzriprnglem6  21825  pzriprnglem12  21831  mat1dimmul  22824  txcnp  23972  upxp  23975  uptx  23977  hauseqlcld  23998  txlm  24000  txkgen  24004  cnmpt1t  24017  cnmpt2t  24025  txhmeo  24155  flfcnp2  24359  ucnimalem  24631  ucnima  24632  fmucndlem  24642  fmucnd  24643  cnheiborlem  25308  pi1xfrcnvlem  25410  ovollb2lem  25842  ovollb2  25843  ovolshftlem2  25864  ovolscalem2  25868  ioombl1  25916  ioorf  25927  ioorval  25928  ioorinv2  25929  uniioombllem6  25942  dyadval  25946  opnmbl  25956  mbfimaopnlem  26009  limccnp2  26245  mpodvdsmulf1o  27554  dvdsmulf1o  27556  precsexlemcbv  28625  precsexlem3  28628  seqseq123d  28705  om2noseqrdg  28723  noseqrdgsuc  28727  ebtwntg  29593  numclwwlk1lem2fv  30990  numclwwlk1lem2fo  30992  numclwwlk1lem2  30994  wlkl0  31001  hhssnvt  31900  hhsssh  31904  opsbc2ie  33147  opreu2reuALT  33148  opfv  33313  xppreima  33314  2ndresdju  33318  aciunf1lem  33331  ofpreima  33334  fgreu  33340  gsumwrd2dccatlem  33714  gsumwrd2dccat  33715  rlocval  33896  rlocaddval  33906  rlocmulval  33907  rloccring  33908  rloc0g  33909  rloc1r  33910  rlocf1  33911  rlocinvunit  33912  rlocisunit  33913  zringfrac  34169  smatlem  34512  qtophaus  34551  qqhval2  34697  esum2dlem  34807  rrvadd  35167  hgt750lemb  35368  bnj1442  35762  bnj1450  35763  bnj1463  35768  bnj1529  35783  maxssj0  36019  erdszelem9  36144  erdszelem10  36145  txpconn  36177  txsconnlem  36185  goaleq12d  36296  msubval  36470  msubco  36476  mvhval  36479  msubvrs  36505  cbvoprab123vw  37219  cbvoprab23vw  37220  cbvoprab13vw  37221  cbvopabdavw  37246  cbvoprab123davw  37254  cbvoprab12davw  37255  cbvoprab23davw  37256  cbvoprab13davw  37257  bj-dfid2ALT  38184  bj-endval  38441  finxpreclem3  38521  poimirlem4  38747  opnmbllem0  38779  mblfinlem1  38780  mblfinlem2  38781  heiborlem6  38953  heiborlem7  38954  heiborlem8  38955  nfopdALT  40231  dvhvaddcbv  42349  dvhvaddval  42350  dvhopvadd  42353  dvhvaddcomN  42356  dvhvaddass  42357  dvhvscacbv  42358  dvhvscaval  42359  dvhopvsca  42362  dvhgrp  42367  dvhlveclem  42368  dvh0g  42371  dvhopaddN  42374  dvhopspN  42375  dvhopN  42376  cdlemn4  42458  hdmapffval  43086  pellexlem3  44042  pellex  44046  elcnvlem  44804  dvnprodlem1  47171  dvnprodlem3  47173  etransclem44  47503  ovolval4  47876  ovolval5lem3  47879  aoveq123d  48463  prproropf1olem2  48801  prproropf1olem3  48802  prproropf1olem4  48803  prproropf1o  48804  prproropreud  48806  isisubgr  49175  eloprab1st2nd  50194  ssccatid  50401  oppfvalg  50457  imaf1co  50486  uptrlem1  50541  xpcfucco3  50595  dfswapf2  50598  swapfval  50599  swapfcoa  50618  1stfpropd  50627  2ndfpropd  50628  tposcurf1  50636  diag1  50641  fuco2eld2  50651  fucofvalg  50655  fuco21  50673  fuco11bALT  50675  fuco23  50678  fuco22natlem3  50681  fuco22nat  50683  fucoid  50685  fuco22a  50687  fucocolem2  50691  fucocolem4  50693  postcofval  50711  precofval  50717  precofvalALT  50718  precofval3  50721  prcofvalg  50726  prcofpropd  50729  prcofdiag1  50743  prcofdiag  50744  fucoppcco  50759  oppfdiag1  50764  oppfdiag  50766  termcfuncval  50882  diag1f1olem  50883  termcfunc1eq  50885  mndtcval  50932  mndtcco  50938  2arwcatlem2  50949  2arwcatlem3  50950  2arwcatlem4  50951  2arwcat  50953  setc1onsubc  50955  parmapfunc2  50989  parmapfunc  50990  lanfval  51011  ranfval  51012  ranup  51040  concom  51061  islmd  51063