Theorem opeq12d 4837

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  nfopd  4846  moop2  5450  iunopeqop  5469  dfid2  5521  fsn2g  7083  funopsn  7093  fnprb  7154  fntpb  7155  fnpr2g  7156  fliftfuns  7260  dfmpo  8044  fsplit  8059  fsplitfpar  8060  fnwelem  8073  fimaproj  8077  seqomlem0  8380  seqomlem1  8381  seqomlem4  8384  qliftfuns  8741  xpassen  8999  xpdom2  9000  xpf1o  9067  xpmapenlem  9072  xpmapen  9073  mapunen  9074  xpwdomg  9490  fseqenlem2  9935  nqereu  10840  addpipq2  10847  addpipq  10848  mulpipq2  10850  mulpipq  10851  1nqenq  10873  mulidnq  10874  ltexnq  10886  prlem934  10944  addsrmo  10984  mulsrmo  10985  addsrpr  10986  mulsrpr  10987  mulcnsr  11047  mulresr  11050  axcnre  11075  om2uzrdg  13879  uzrdgsuci  13883  pfxsuff1eqwrdeq  14622  swrdpfx  14630  ccatopth  14639  swrdccatin2d  14667  splval  14674  splcl  14675  cshfn  14713  repswcshw  14735  2swrd2eqwrdeq  14876  ruclem1  16156  eucalgval2  16508  qnumdenbi  16671  crth  16705  phimullem  16706  prmreclem3  16846  setsstruct  17103  ressval3d  17173  imasval  17432  imasaddvallem  17450  xpsff1o  17488  catidex  17597  cidval  17600  catcocl  17608  catass  17609  oppccofval  17639  sectfval  17675  subccocl  17769  isfunc  17788  funcco  17795  idfuval  17800  idfucl  17805  cofuval  17806  cofuval2  17811  cofucl  17812  cofuass  17813  cofulid  17814  cofurid  17815  resfval  17816  resfval2  17817  funcres  17820  inclfusubc  17867  isnat  17874  nati  17882  fucco  17889  fuccoval  17890  coaval  17992  catcisolem  18034  xpcval  18100  xpcco  18106  xpcco2  18110  xpccatid  18111  xpcid  18112  1stfval  18114  2ndfval  18117  1stfcl  18120  2ndfcl  18121  prfval  18122  prf1  18123  prf2fval  18124  prf2  18125  prfcl  18126  prf1st  18127  prf2nd  18128  1st2ndprf  18129  xpcpropd  18131  evlfval  18140  evlf2  18141  evlfcllem  18144  evlfcl  18145  curfval  18146  curf1  18148  curf1cl  18151  curf2cl  18154  curfcl  18155  curfpropd  18156  uncf1  18159  uncf2  18160  curfuncf  18161  uncfcurf  18162  diagval  18163  curf2ndf  18170  hofval  18175  hof2fval  18178  hofcl  18182  yonval  18184  hofpropd  18190  yonedalem21  18196  yonedalem22  18201  yonedalem3  18203  xpsmnd0  18703  xpsinv  18990  xpsgrpsub  18991  symg2bas  19322  xpsring1d  20269  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  rngqiprngimfv  21253  rngqiprngghm  21254  rngqiprngimf1  21255  rngqiprngimfo  21256  rngqiprnglin  21257  rngqipring1  21271  rngqiprngfu  21272  pzriprnglem6  21441  pzriprnglem12  21447  mat1dimmul  22420  txcnp  23564  upxp  23567  uptx  23569  hauseqlcld  23590  txlm  23592  txkgen  23596  cnmpt1t  23609  cnmpt2t  23617  txhmeo  23747  flfcnp2  23951  ucnimalem  24223  ucnima  24224  fmucndlem  24234  fmucnd  24235  cnheiborlem  24909  pi1xfrcnvlem  25012  ovollb2lem  25445  ovollb2  25446  ovolshftlem2  25467  ovolscalem2  25471  ioombl1  25519  ioorf  25530  ioorval  25531  ioorinv2  25532  uniioombllem6  25545  dyadval  25549  opnmbl  25559  mbfimaopnlem  25612  limccnp2  25849  mpodvdsmulf1o  27160  dvdsmulf1o  27162  precsexlemcbv  28202  precsexlem3  28205  seqseq123d  28282  om2noseqrdg  28300  noseqrdgsuc  28304  ebtwntg  29055  numclwwlk1lem2fv  30431  numclwwlk1lem2fo  30433  numclwwlk1lem2  30435  wlkl0  30442  hhssnvt  31340  hhsssh  31344  opsbc2ie  32550  opreu2reuALT  32551  opfv  32722  xppreima  32723  2ndresdju  32727  aciunf1lem  32740  ofpreima  32743  fgreu  32750  gsumwrd2dccatlem  33159  gsumwrd2dccat  33160  rlocval  33341  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  zringfrac  33635  smatlem  33954  qtophaus  33993  qqhval2  34139  esum2dlem  34249  rrvadd  34609  hgt750lemb  34813  bnj1442  35205  bnj1450  35206  bnj1463  35211  bnj1529  35226  swrdrevpfx  35311  erdszelem9  35393  erdszelem10  35394  txpconn  35426  txsconnlem  35434  goaleq12d  35545  msubval  35719  msubco  35725  mvhval  35728  msubvrs  35754  cbvoprab123vw  36433  cbvoprab23vw  36434  cbvoprab13vw  36435  cbvopabdavw  36460  cbvoprab123davw  36468  cbvoprab12davw  36469  cbvoprab23davw  36470  cbvoprab13davw  36471  bj-dfid2ALT  37266  bj-endval  37516  finxpreclem3  37594  poimirlem4  37821  opnmbllem0  37853  mblfinlem1  37854  mblfinlem2  37855  heiborlem6  38013  heiborlem7  38014  heiborlem8  38015  nfopdALT  39227  dvhvaddcbv  41345  dvhvaddval  41346  dvhopvadd  41349  dvhvaddcomN  41352  dvhvaddass  41353  dvhvscacbv  41354  dvhvscaval  41355  dvhopvsca  41358  dvhgrp  41363  dvhlveclem  41364  dvh0g  41367  dvhopaddN  41370  dvhopspN  41371  dvhopN  41372  cdlemn4  41454  hdmapffval  42082  pellexlem3  43069  pellex  43073  elcnvlem  43838  dvnprodlem1  46186  dvnprodlem3  46188  etransclem44  46518  ovolval4  46891  ovolval5lem3  46894  aoveq123d  47420  prproropf1olem2  47746  prproropf1olem3  47747  prproropf1olem4  47748  prproropf1o  47749  prproropreud  47751  isisubgr  48104  eloprab1st2nd  49109  ssccatid  49313  oppfvalg  49367  imaf1co  49396  uptrlem1  49451  xpcfucco3  49499  dfswapf2  49502  swapfval  49503  swapfcoa  49522  1stfpropd  49531  2ndfpropd  49532  tposcurf1  49540  diag1  49545  fuco2eld2  49555  fucofvalg  49559  fuco21  49577  fuco11bALT  49579  fuco23  49582  fuco22natlem3  49585  fuco22nat  49587  fucoid  49589  fuco22a  49591  fucocolem2  49595  fucocolem4  49597  postcofval  49605  precofval  49608  precofvalALT  49609  precofval3  49612  prcofvalg  49617  prcofpropd  49620  prcofdiag1  49634  prcofdiag  49635  fucoppcco  49650  oppfdiag1  49655  oppfdiag  49657  termcfuncval  49773  diag1f1olem  49774  mndtcval  49820  mndtcco  49826  2arwcatlem2  49837  2arwcatlem3  49838  2arwcatlem4  49839  2arwcat  49841  setc1onsubc  49843  lanfval  49854  ranfval  49855  ranup  49883  concom  49904  islmd  49906