Theorem opeq12d 4817

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573

This theorem is referenced by:  nfopd  4826  moop2  5418  iunopeqop  5437  dfid2  5490  fsn2g  7004  funopsn  7014  fnprb  7078  fntpb  7079  fnpr2g  7080  fliftfuns  7178  dfmpo  7926  fsplit  7941  fsplitOLD  7942  fsplitfpar  7943  fnwelem  7956  fimaproj  7960  seqomlem0  8264  seqomlem1  8265  seqomlem4  8268  qliftfuns  8567  xpassen  8822  xpdom2  8823  xpf1o  8891  xpmapenlem  8896  xpmapen  8897  mapunen  8898  xpwdomg  9305  fseqenlem2  9765  nqereu  10669  addpipq2  10676  addpipq  10677  mulpipq2  10679  mulpipq  10680  1nqenq  10702  mulidnq  10703  ltexnq  10715  prlem934  10773  addsrmo  10813  mulsrmo  10814  addsrpr  10815  mulsrpr  10816  mulcnsr  10876  mulresr  10879  axcnre  10904  om2uzrdg  13657  uzrdgsuci  13661  pfxsuff1eqwrdeq  14393  swrdpfx  14401  ccatopth  14410  swrdccatin2d  14438  splval  14445  splcl  14446  cshfn  14484  repswcshw  14506  2swrd2eqwrdeq  14647  ruclem1  15921  eucalgval2  16267  qnumdenbi  16429  crth  16460  phimullem  16461  prmreclem3  16600  setsstruct  16858  ressval3d  16937  ressval3dOLD  16938  imasval  17203  imasaddvallem  17221  xpsff1o  17259  catidex  17364  cidval  17367  catcocl  17375  catass  17376  oppccofval  17407  sectfval  17444  subccocl  17541  isfunc  17560  funcco  17567  idfuval  17572  idfucl  17577  cofuval  17578  cofuval2  17583  cofucl  17584  cofuass  17585  cofulid  17586  cofurid  17587  resfval  17588  resfval2  17589  funcres  17592  isnat  17644  nati  17652  fucco  17661  fuccoval  17662  coaval  17764  catcisolem  17806  xpcval  17875  xpcco  17881  xpcco2  17885  xpccatid  17886  xpcid  17887  1stfval  17889  2ndfval  17892  1stfcl  17895  2ndfcl  17896  prfval  17897  prf1  17898  prf2fval  17899  prf2  17900  prfcl  17901  prf1st  17902  prf2nd  17903  1st2ndprf  17904  xpcpropd  17907  evlfval  17916  evlf2  17917  evlfcllem  17920  evlfcl  17921  curfval  17922  curf1  17924  curf1cl  17927  curf2cl  17930  curfcl  17931  curfpropd  17932  uncf1  17935  uncf2  17936  curfuncf  17937  uncfcurf  17938  diagval  17939  curf2ndf  17946  hofval  17951  hof2fval  17954  hofcl  17958  yonval  17960  hofpropd  17966  yonedalem21  17972  yonedalem22  17977  yonedalem3  17979  symg2bas  18981  mat1dimmul  21606  txcnp  22752  upxp  22755  uptx  22757  hauseqlcld  22778  txlm  22780  txkgen  22784  cnmpt1t  22797  cnmpt2t  22805  txhmeo  22935  flfcnp2  23139  ucnimalem  23413  ucnima  23414  fmucndlem  23424  fmucnd  23425  cnheiborlem  24098  pi1xfrcnvlem  24200  ovollb2lem  24633  ovollb2  24634  ovolshftlem2  24655  ovolscalem2  24659  ioombl1  24707  ioorf  24718  ioorval  24719  ioorinv2  24720  uniioombllem6  24733  dyadval  24737  opnmbl  24747  mbfimaopnlem  24800  limccnp2  25037  dvdsmulf1o  26324  ebtwntg  27331  numclwwlk1lem2fv  28699  numclwwlk1lem2fo  28701  numclwwlk1lem2  28703  wlkl0  28710  hhssnvt  29606  hhsssh  29610  opsbc2ie  30803  opreu2reuALT  30804  opfv  30961  xppreima  30962  2ndresdju  30965  aciunf1lem  30978  ofpreima  30981  fgreu  30988  smatlem  31726  qtophaus  31765  qqhval2  31911  esum2dlem  32039  rrvadd  32398  hgt750lemb  32615  bnj1442  33008  bnj1450  33009  bnj1463  33014  bnj1529  33029  swrdrevpfx  33057  erdszelem9  33140  erdszelem10  33141  txpconn  33173  txsconnlem  33181  goaleq12d  33292  msubval  33466  msubco  33472  mvhval  33475  msubvrs  33501  bj-dfid2ALT  35215  bj-endval  35465  finxpreclem3  35543  poimirlem4  35760  opnmbllem0  35792  mblfinlem1  35793  mblfinlem2  35794  heiborlem6  35953  heiborlem7  35954  heiborlem8  35955  nfopdALT  36964  dvhvaddcbv  39082  dvhvaddval  39083  dvhopvadd  39086  dvhvaddcomN  39089  dvhvaddass  39090  dvhvscacbv  39091  dvhvscaval  39092  dvhopvsca  39095  dvhgrp  39100  dvhlveclem  39101  dvh0g  39104  dvhopaddN  39107  dvhopspN  39108  dvhopN  39109  cdlemn4  39191  hdmapffval  39819  pellexlem3  40633  pellex  40637  elcnvlem  41162  dvnprodlem1  43441  dvnprodlem3  43443  etransclem44  43773  ovolval4  44143  ovolval5lem3  44146  aoveq123d  44621  prproropf1olem2  44908  prproropf1olem3  44909  prproropf1olem4  44910  prproropf1o  44911  prproropreud  44913  inclfusubc  45377  funcrngcsetc  45508  funcrngcsetcALT  45509  funcringcsetc  45545  mndtcval  46318  mndtcco  46324