Theorem opeq12d 4835

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  nfopd  4844  moop2  5449  iunopeqop  5468  dfid2  5520  fsn2g  7076  funopsn  7086  fnprb  7148  fntpb  7149  fnpr2g  7150  fliftfuns  7255  dfmpo  8042  fsplit  8057  fsplitfpar  8058  fnwelem  8071  fimaproj  8075  seqomlem0  8378  seqomlem1  8379  seqomlem4  8382  qliftfuns  8738  xpassen  8995  xpdom2  8996  xpf1o  9063  xpmapenlem  9068  xpmapen  9069  mapunen  9070  xpwdomg  9496  fseqenlem2  9938  nqereu  10842  addpipq2  10849  addpipq  10850  mulpipq2  10852  mulpipq  10853  1nqenq  10875  mulidnq  10876  ltexnq  10888  prlem934  10946  addsrmo  10986  mulsrmo  10987  addsrpr  10988  mulsrpr  10989  mulcnsr  11049  mulresr  11052  axcnre  11077  om2uzrdg  13881  uzrdgsuci  13885  pfxsuff1eqwrdeq  14623  swrdpfx  14631  ccatopth  14640  swrdccatin2d  14668  splval  14675  splcl  14676  cshfn  14714  repswcshw  14736  2swrd2eqwrdeq  14878  ruclem1  16158  eucalgval2  16510  qnumdenbi  16673  crth  16707  phimullem  16708  prmreclem3  16848  setsstruct  17105  ressval3d  17175  imasval  17433  imasaddvallem  17451  xpsff1o  17489  catidex  17598  cidval  17601  catcocl  17609  catass  17610  oppccofval  17640  sectfval  17676  subccocl  17770  isfunc  17789  funcco  17796  idfuval  17801  idfucl  17806  cofuval  17807  cofuval2  17812  cofucl  17813  cofuass  17814  cofulid  17815  cofurid  17816  resfval  17817  resfval2  17818  funcres  17821  inclfusubc  17868  isnat  17875  nati  17883  fucco  17890  fuccoval  17891  coaval  17993  catcisolem  18035  xpcval  18101  xpcco  18107  xpcco2  18111  xpccatid  18112  xpcid  18113  1stfval  18115  2ndfval  18118  1stfcl  18121  2ndfcl  18122  prfval  18123  prf1  18124  prf2fval  18125  prf2  18126  prfcl  18127  prf1st  18128  prf2nd  18129  1st2ndprf  18130  xpcpropd  18132  evlfval  18141  evlf2  18142  evlfcllem  18145  evlfcl  18146  curfval  18147  curf1  18149  curf1cl  18152  curf2cl  18155  curfcl  18156  curfpropd  18157  uncf1  18160  uncf2  18161  curfuncf  18162  uncfcurf  18163  diagval  18164  curf2ndf  18171  hofval  18176  hof2fval  18179  hofcl  18183  yonval  18185  hofpropd  18191  yonedalem21  18197  yonedalem22  18202  yonedalem3  18204  xpsmnd0  18670  xpsinv  18957  xpsgrpsub  18958  symg2bas  19290  xpsring1d  20236  funcrngcsetc  20543  funcrngcsetcALT  20544  funcringcsetc  20577  rngqiprngimfv  21223  rngqiprngghm  21224  rngqiprngimf1  21225  rngqiprngimfo  21226  rngqiprnglin  21227  rngqipring1  21241  rngqiprngfu  21242  pzriprnglem6  21411  pzriprnglem12  21417  mat1dimmul  22379  txcnp  23523  upxp  23526  uptx  23528  hauseqlcld  23549  txlm  23551  txkgen  23555  cnmpt1t  23568  cnmpt2t  23576  txhmeo  23706  flfcnp2  23910  ucnimalem  24183  ucnima  24184  fmucndlem  24194  fmucnd  24195  cnheiborlem  24869  pi1xfrcnvlem  24972  ovollb2lem  25405  ovollb2  25406  ovolshftlem2  25427  ovolscalem2  25431  ioombl1  25479  ioorf  25490  ioorval  25491  ioorinv2  25492  uniioombllem6  25505  dyadval  25509  opnmbl  25519  mbfimaopnlem  25572  limccnp2  25809  mpodvdsmulf1o  27120  dvdsmulf1o  27122  precsexlemcbv  28131  precsexlem3  28134  seqseq123d  28203  om2noseqrdg  28221  noseqrdgsuc  28225  ebtwntg  28945  numclwwlk1lem2fv  30318  numclwwlk1lem2fo  30320  numclwwlk1lem2  30322  wlkl0  30329  hhssnvt  31227  hhsssh  31231  opsbc2ie  32438  opreu2reuALT  32439  opfv  32601  xppreima  32602  2ndresdju  32606  aciunf1lem  32619  ofpreima  32622  fgreu  32629  gsumwrd2dccatlem  33032  gsumwrd2dccat  33033  rlocval  33209  rlocaddval  33218  rlocmulval  33219  rloccring  33220  rloc0g  33221  rloc1r  33222  rlocf1  33223  zringfrac  33501  smatlem  33763  qtophaus  33802  qqhval2  33948  esum2dlem  34058  rrvadd  34419  hgt750lemb  34623  bnj1442  35015  bnj1450  35016  bnj1463  35021  bnj1529  35036  swrdrevpfx  35089  erdszelem9  35171  erdszelem10  35172  txpconn  35204  txsconnlem  35212  goaleq12d  35323  msubval  35497  msubco  35503  mvhval  35506  msubvrs  35532  cbvoprab123vw  36212  cbvoprab23vw  36213  cbvoprab13vw  36214  cbvopabdavw  36239  cbvoprab123davw  36247  cbvoprab12davw  36248  cbvoprab23davw  36249  cbvoprab13davw  36250  bj-dfid2ALT  37038  bj-endval  37288  finxpreclem3  37366  poimirlem4  37603  opnmbllem0  37635  mblfinlem1  37636  mblfinlem2  37637  heiborlem6  37795  heiborlem7  37796  heiborlem8  37797  nfopdALT  38949  dvhvaddcbv  41068  dvhvaddval  41069  dvhopvadd  41072  dvhvaddcomN  41075  dvhvaddass  41076  dvhvscacbv  41077  dvhvscaval  41078  dvhopvsca  41081  dvhgrp  41086  dvhlveclem  41087  dvh0g  41090  dvhopaddN  41093  dvhopspN  41094  dvhopN  41095  cdlemn4  41177  hdmapffval  41805  pellexlem3  42804  pellex  42808  elcnvlem  43574  dvnprodlem1  45928  dvnprodlem3  45930  etransclem44  46260  ovolval4  46633  ovolval5lem3  46636  aoveq123d  47163  prproropf1olem2  47489  prproropf1olem3  47490  prproropf1olem4  47491  prproropf1o  47492  prproropreud  47494  isisubgr  47847  eloprab1st2nd  48853  ssccatid  49058  oppfvalg  49112  imaf1co  49141  uptrlem1  49196  xpcfucco3  49244  dfswapf2  49247  swapfval  49248  swapfcoa  49267  1stfpropd  49276  2ndfpropd  49277  tposcurf1  49285  diag1  49290  fuco2eld2  49300  fucofvalg  49304  fuco21  49322  fuco11bALT  49324  fuco23  49327  fuco22natlem3  49330  fuco22nat  49332  fucoid  49334  fuco22a  49336  fucocolem2  49340  fucocolem4  49342  postcofval  49350  precofval  49353  precofvalALT  49354  precofval3  49357  prcofvalg  49362  prcofpropd  49365  prcofdiag1  49379  prcofdiag  49380  fucoppcco  49395  oppfdiag1  49400  oppfdiag  49402  termcfuncval  49518  diag1f1olem  49519  mndtcval  49565  mndtcco  49571  2arwcatlem2  49582  2arwcatlem3  49583  2arwcatlem4  49584  2arwcat  49586  setc1onsubc  49588  lanfval  49599  ranfval  49600  ranup  49628  concom  49649  islmd  49651