Theorem opeq12d 4819

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

Syntax hints:   → wi 4   = wceq 1547  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  nfopd  4828  moop2  5450  iunopeqop  5469  iunopeqopOLD  5470  dfid2  5522  fsn2g  7087  funopsn  7097  funopsnOLD  7098  fnprb  7159  fntpb  7160  fnpr2g  7161  fliftfuns  7265  dfmpo  8048  fsplit  8063  fsplitfpar  8064  fnwelem  8078  fimaproj  8082  seqomlem0  8385  seqomlem1  8386  seqomlem4  8389  qliftfuns  8748  xpassen  9006  xpdom2  9007  xpf1o  9074  xpmapenlem  9079  xpmapen  9080  mapunen  9081  xpwdomg  9497  fseqenlem2  9945  nqereu  10850  addpipq2  10857  addpipq  10858  mulpipq2  10860  mulpipq  10861  1nqenq  10883  mulidnq  10884  ltexnq  10896  prlem934  10954  addsrmo  10994  mulsrmo  10995  addsrpr  10996  mulsrpr  10997  mulcnsr  11057  mulresr  11060  axcnre  11085  om2uzrdg  13916  uzrdgsuci  13920  pfxsuff1eqwrdeq  14659  swrdpfx  14667  ccatopth  14676  swrdccatin2d  14704  splval  14711  splcl  14712  cshfn  14750  repswcshw  14772  2swrd2eqwrdeq  14913  ruclem1  16196  eucalgval2  16548  qnumdenbi  16712  crth  16746  phimullem  16747  prmreclem3  16887  setsstruct  17144  ressval3d  17214  imasval  17473  imasaddvallem  17491  xpsff1o  17529  catidex  17638  cidval  17641  catcocl  17649  catass  17650  oppccofval  17680  sectfval  17716  subccocl  17810  isfunc  17829  funcco  17836  idfuval  17841  idfucl  17846  cofuval  17847  cofuval2  17852  cofucl  17853  cofuass  17854  cofulid  17855  cofurid  17856  resfval  17857  resfval2  17858  funcres  17861  inclfusubc  17908  isnat  17915  nati  17923  fucco  17930  fuccoval  17931  coaval  18033  catcisolem  18075  xpcval  18141  xpcco  18147  xpcco2  18151  xpccatid  18152  xpcid  18153  1stfval  18155  2ndfval  18158  1stfcl  18161  2ndfcl  18162  prfval  18163  prf1  18164  prf2fval  18165  prf2  18166  prfcl  18167  prf1st  18168  prf2nd  18169  1st2ndprf  18170  xpcpropd  18172  evlfval  18181  evlf2  18182  evlfcllem  18185  evlfcl  18186  curfval  18187  curf1  18189  curf1cl  18192  curf2cl  18195  curfcl  18196  curfpropd  18197  uncf1  18200  uncf2  18201  curfuncf  18202  uncfcurf  18203  diagval  18204  curf2ndf  18211  hofval  18216  hof2fval  18219  hofcl  18223  yonval  18225  hofpropd  18231  yonedalem21  18237  yonedalem22  18242  yonedalem3  18244  xpsmnd0  18744  xpsinv  19034  xpsgrpsub  19035  symg2bas  19366  xpsring1d  20311  funcrngcsetc  20619  funcrngcsetcALT  20620  funcringcsetc  20653  rngqiprngimfv  21298  rngqiprngghm  21299  rngqiprngimf1  21300  rngqiprngimfo  21301  rngqiprnglin  21302  rngqipring1  21316  rngqiprngfu  21317  pzriprnglem6  21468  pzriprnglem12  21474  mat1dimmul  22466  txcnp  23610  upxp  23613  uptx  23615  hauseqlcld  23636  txlm  23638  txkgen  23642  cnmpt1t  23655  cnmpt2t  23663  txhmeo  23793  flfcnp2  23997  ucnimalem  24269  ucnima  24270  fmucndlem  24280  fmucnd  24281  cnheiborlem  24946  pi1xfrcnvlem  25048  ovollb2lem  25480  ovollb2  25481  ovolshftlem2  25502  ovolscalem2  25506  ioombl1  25554  ioorf  25565  ioorval  25566  ioorinv2  25567  uniioombllem6  25580  dyadval  25584  opnmbl  25594  mbfimaopnlem  25647  limccnp2  25884  mpodvdsmulf1o  27182  dvdsmulf1o  27184  precsexlemcbv  28223  precsexlem3  28226  seqseq123d  28303  om2noseqrdg  28321  noseqrdgsuc  28325  ebtwntg  29076  numclwwlk1lem2fv  30451  numclwwlk1lem2fo  30453  numclwwlk1lem2  30455  wlkl0  30462  hhssnvt  31361  hhsssh  31365  opsbc2ie  32570  opreu2reuALT  32571  opfv  32743  xppreima  32744  2ndresdju  32748  aciunf1lem  32761  ofpreima  32764  fgreu  32770  gsumwrd2dccatlem  33165  gsumwrd2dccat  33166  rlocval  33347  rlocaddval  33356  rlocmulval  33357  rloccring  33358  rloc0g  33359  rloc1r  33360  rlocf1  33361  zringfrac  33644  smatlem  33988  qtophaus  34027  qqhval2  34173  esum2dlem  34283  rrvadd  34643  hgt750lemb  34847  bnj1442  35238  bnj1450  35239  bnj1463  35244  bnj1529  35259  swrdrevpfx  35352  erdszelem9  35434  erdszelem10  35435  txpconn  35467  txsconnlem  35475  goaleq12d  35586  msubval  35760  msubco  35766  mvhval  35769  msubvrs  35795  cbvoprab123vw  36474  cbvoprab23vw  36475  cbvoprab13vw  36476  cbvopabdavw  36501  cbvoprab123davw  36509  cbvoprab12davw  36510  cbvoprab23davw  36511  cbvoprab13davw  36512  bj-dfid2ALT  37425  bj-endval  37682  finxpreclem3  37762  poimirlem4  37998  opnmbllem0  38030  mblfinlem1  38031  mblfinlem2  38032  heiborlem6  38190  heiborlem7  38191  heiborlem8  38192  nfopdALT  39470  dvhvaddcbv  41588  dvhvaddval  41589  dvhopvadd  41592  dvhvaddcomN  41595  dvhvaddass  41596  dvhvscacbv  41597  dvhvscaval  41598  dvhopvsca  41601  dvhgrp  41606  dvhlveclem  41607  dvh0g  41610  dvhopaddN  41613  dvhopspN  41614  dvhopN  41615  cdlemn4  41697  hdmapffval  42325  pellexlem3  43283  pellex  43287  elcnvlem  44052  dvnprodlem1  46396  dvnprodlem3  46398  etransclem44  46728  ovolval4  47101  ovolval5lem3  47104  aoveq123d  47648  prproropf1olem2  47986  prproropf1olem3  47987  prproropf1olem4  47988  prproropf1o  47989  prproropreud  47991  isisubgr  48360  eloprab1st2nd  49365  ssccatid  49569  oppfvalg  49623  imaf1co  49652  uptrlem1  49707  xpcfucco3  49755  dfswapf2  49758  swapfval  49759  swapfcoa  49778  1stfpropd  49787  2ndfpropd  49788  tposcurf1  49796  diag1  49801  fuco2eld2  49811  fucofvalg  49815  fuco21  49833  fuco11bALT  49835  fuco23  49838  fuco22natlem3  49841  fuco22nat  49843  fucoid  49845  fuco22a  49847  fucocolem2  49851  fucocolem4  49853  postcofval  49861  precofval  49864  precofvalALT  49865  precofval3  49868  prcofvalg  49873  prcofpropd  49876  prcofdiag1  49890  prcofdiag  49891  fucoppcco  49906  oppfdiag1  49911  oppfdiag  49913  termcfuncval  50029  diag1f1olem  50030  mndtcval  50076  mndtcco  50082  2arwcatlem2  50093  2arwcatlem3  50094  2arwcatlem4  50095  2arwcat  50097  setc1onsubc  50099  lanfval  50110  ranfval  50111  ranup  50139  concom  50160  islmd  50162