Theorem opeq12d 4839

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4588

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  nfopd  4848  moop2  5458  iunopeqop  5477  dfid2  5529  fsn2g  7093  funopsn  7103  fnprb  7164  fntpb  7165  fnpr2g  7166  fliftfuns  7270  dfmpo  8054  fsplit  8069  fsplitfpar  8070  fnwelem  8083  fimaproj  8087  seqomlem0  8390  seqomlem1  8391  seqomlem4  8394  qliftfuns  8753  xpassen  9011  xpdom2  9012  xpf1o  9079  xpmapenlem  9084  xpmapen  9085  mapunen  9086  xpwdomg  9502  fseqenlem2  9947  nqereu  10852  addpipq2  10859  addpipq  10860  mulpipq2  10862  mulpipq  10863  1nqenq  10885  mulidnq  10886  ltexnq  10898  prlem934  10956  addsrmo  10996  mulsrmo  10997  addsrpr  10998  mulsrpr  10999  mulcnsr  11059  mulresr  11062  axcnre  11087  om2uzrdg  13891  uzrdgsuci  13895  pfxsuff1eqwrdeq  14634  swrdpfx  14642  ccatopth  14651  swrdccatin2d  14679  splval  14686  splcl  14687  cshfn  14725  repswcshw  14747  2swrd2eqwrdeq  14888  ruclem1  16168  eucalgval2  16520  qnumdenbi  16683  crth  16717  phimullem  16718  prmreclem3  16858  setsstruct  17115  ressval3d  17185  imasval  17444  imasaddvallem  17462  xpsff1o  17500  catidex  17609  cidval  17612  catcocl  17620  catass  17621  oppccofval  17651  sectfval  17687  subccocl  17781  isfunc  17800  funcco  17807  idfuval  17812  idfucl  17817  cofuval  17818  cofuval2  17823  cofucl  17824  cofuass  17825  cofulid  17826  cofurid  17827  resfval  17828  resfval2  17829  funcres  17832  inclfusubc  17879  isnat  17886  nati  17894  fucco  17901  fuccoval  17902  coaval  18004  catcisolem  18046  xpcval  18112  xpcco  18118  xpcco2  18122  xpccatid  18123  xpcid  18124  1stfval  18126  2ndfval  18129  1stfcl  18132  2ndfcl  18133  prfval  18134  prf1  18135  prf2fval  18136  prf2  18137  prfcl  18138  prf1st  18139  prf2nd  18140  1st2ndprf  18141  xpcpropd  18143  evlfval  18152  evlf2  18153  evlfcllem  18156  evlfcl  18157  curfval  18158  curf1  18160  curf1cl  18163  curf2cl  18166  curfcl  18167  curfpropd  18168  uncf1  18171  uncf2  18172  curfuncf  18173  uncfcurf  18174  diagval  18175  curf2ndf  18182  hofval  18187  hof2fval  18190  hofcl  18194  yonval  18196  hofpropd  18202  yonedalem21  18208  yonedalem22  18213  yonedalem3  18215  xpsmnd0  18715  xpsinv  19002  xpsgrpsub  19003  symg2bas  19334  xpsring1d  20281  funcrngcsetc  20585  funcrngcsetcALT  20586  funcringcsetc  20619  rngqiprngimfv  21265  rngqiprngghm  21266  rngqiprngimf1  21267  rngqiprngimfo  21268  rngqiprnglin  21269  rngqipring1  21283  rngqiprngfu  21284  pzriprnglem6  21453  pzriprnglem12  21459  mat1dimmul  22432  txcnp  23576  upxp  23579  uptx  23581  hauseqlcld  23602  txlm  23604  txkgen  23608  cnmpt1t  23621  cnmpt2t  23629  txhmeo  23759  flfcnp2  23963  ucnimalem  24235  ucnima  24236  fmucndlem  24246  fmucnd  24247  cnheiborlem  24921  pi1xfrcnvlem  25024  ovollb2lem  25457  ovollb2  25458  ovolshftlem2  25479  ovolscalem2  25483  ioombl1  25531  ioorf  25542  ioorval  25543  ioorinv2  25544  uniioombllem6  25557  dyadval  25561  opnmbl  25571  mbfimaopnlem  25624  limccnp2  25861  mpodvdsmulf1o  27172  dvdsmulf1o  27174  precsexlemcbv  28214  precsexlem3  28217  seqseq123d  28294  om2noseqrdg  28312  noseqrdgsuc  28316  ebtwntg  29067  numclwwlk1lem2fv  30443  numclwwlk1lem2fo  30445  numclwwlk1lem2  30447  wlkl0  30454  hhssnvt  31352  hhsssh  31356  opsbc2ie  32561  opreu2reuALT  32562  opfv  32733  xppreima  32734  2ndresdju  32738  aciunf1lem  32751  ofpreima  32754  fgreu  32760  gsumwrd2dccatlem  33170  gsumwrd2dccat  33171  rlocval  33352  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rloc0g  33364  rloc1r  33365  rlocf1  33366  zringfrac  33646  smatlem  33974  qtophaus  34013  qqhval2  34159  esum2dlem  34269  rrvadd  34629  hgt750lemb  34833  bnj1442  35224  bnj1450  35225  bnj1463  35230  bnj1529  35245  swrdrevpfx  35330  erdszelem9  35412  erdszelem10  35413  txpconn  35445  txsconnlem  35453  goaleq12d  35564  msubval  35738  msubco  35744  mvhval  35747  msubvrs  35773  cbvoprab123vw  36452  cbvoprab23vw  36453  cbvoprab13vw  36454  cbvopabdavw  36479  cbvoprab123davw  36487  cbvoprab12davw  36488  cbvoprab23davw  36489  cbvoprab13davw  36490  bj-dfid2ALT  37307  bj-endval  37564  finxpreclem3  37642  poimirlem4  37869  opnmbllem0  37901  mblfinlem1  37902  mblfinlem2  37903  heiborlem6  38061  heiborlem7  38062  heiborlem8  38063  nfopdALT  39341  dvhvaddcbv  41459  dvhvaddval  41460  dvhopvadd  41463  dvhvaddcomN  41466  dvhvaddass  41467  dvhvscacbv  41468  dvhvscaval  41469  dvhopvsca  41472  dvhgrp  41477  dvhlveclem  41478  dvh0g  41481  dvhopaddN  41484  dvhopspN  41485  dvhopN  41486  cdlemn4  41568  hdmapffval  42196  pellexlem3  43182  pellex  43186  elcnvlem  43951  dvnprodlem1  46298  dvnprodlem3  46300  etransclem44  46630  ovolval4  47003  ovolval5lem3  47006  aoveq123d  47532  prproropf1olem2  47858  prproropf1olem3  47859  prproropf1olem4  47860  prproropf1o  47861  prproropreud  47863  isisubgr  48216  eloprab1st2nd  49221  ssccatid  49425  oppfvalg  49479  imaf1co  49508  uptrlem1  49563  xpcfucco3  49611  dfswapf2  49614  swapfval  49615  swapfcoa  49634  1stfpropd  49643  2ndfpropd  49644  tposcurf1  49652  diag1  49657  fuco2eld2  49667  fucofvalg  49671  fuco21  49689  fuco11bALT  49691  fuco23  49694  fuco22natlem3  49697  fuco22nat  49699  fucoid  49701  fuco22a  49703  fucocolem2  49707  fucocolem4  49709  postcofval  49717  precofval  49720  precofvalALT  49721  precofval3  49724  prcofvalg  49729  prcofpropd  49732  prcofdiag1  49746  prcofdiag  49747  fucoppcco  49762  oppfdiag1  49767  oppfdiag  49769  termcfuncval  49885  diag1f1olem  49886  mndtcval  49932  mndtcco  49938  2arwcatlem2  49949  2arwcatlem3  49950  2arwcatlem4  49951  2arwcat  49953  setc1onsubc  49955  lanfval  49966  ranfval  49967  ranup  49995  concom  50016  islmd  50018