Theorem opeq12d 4848

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  nfopd  4857  moop2  5465  iunopeqop  5484  dfid2  5538  fsn2g  7113  funopsn  7123  fnprb  7185  fntpb  7186  fnpr2g  7187  fliftfuns  7292  dfmpo  8084  fsplit  8099  fsplitfpar  8100  fnwelem  8113  fimaproj  8117  seqomlem0  8420  seqomlem1  8421  seqomlem4  8424  qliftfuns  8780  xpassen  9040  xpdom2  9041  xpf1o  9109  xpmapenlem  9114  xpmapen  9115  mapunen  9116  xpwdomg  9545  fseqenlem2  9985  nqereu  10889  addpipq2  10896  addpipq  10897  mulpipq2  10899  mulpipq  10900  1nqenq  10922  mulidnq  10923  ltexnq  10935  prlem934  10993  addsrmo  11033  mulsrmo  11034  addsrpr  11035  mulsrpr  11036  mulcnsr  11096  mulresr  11099  axcnre  11124  om2uzrdg  13928  uzrdgsuci  13932  pfxsuff1eqwrdeq  14671  swrdpfx  14679  ccatopth  14688  swrdccatin2d  14716  splval  14723  splcl  14724  cshfn  14762  repswcshw  14784  2swrd2eqwrdeq  14926  ruclem1  16206  eucalgval2  16558  qnumdenbi  16721  crth  16755  phimullem  16756  prmreclem3  16896  setsstruct  17153  ressval3d  17223  imasval  17481  imasaddvallem  17499  xpsff1o  17537  catidex  17642  cidval  17645  catcocl  17653  catass  17654  oppccofval  17684  sectfval  17720  subccocl  17814  isfunc  17833  funcco  17840  idfuval  17845  idfucl  17850  cofuval  17851  cofuval2  17856  cofucl  17857  cofuass  17858  cofulid  17859  cofurid  17860  resfval  17861  resfval2  17862  funcres  17865  inclfusubc  17912  isnat  17919  nati  17927  fucco  17934  fuccoval  17935  coaval  18037  catcisolem  18079  xpcval  18145  xpcco  18151  xpcco2  18155  xpccatid  18156  xpcid  18157  1stfval  18159  2ndfval  18162  1stfcl  18165  2ndfcl  18166  prfval  18167  prf1  18168  prf2fval  18169  prf2  18170  prfcl  18171  prf1st  18172  prf2nd  18173  1st2ndprf  18174  xpcpropd  18176  evlfval  18185  evlf2  18186  evlfcllem  18189  evlfcl  18190  curfval  18191  curf1  18193  curf1cl  18196  curf2cl  18199  curfcl  18200  curfpropd  18201  uncf1  18204  uncf2  18205  curfuncf  18206  uncfcurf  18207  diagval  18208  curf2ndf  18215  hofval  18220  hof2fval  18223  hofcl  18227  yonval  18229  hofpropd  18235  yonedalem21  18241  yonedalem22  18246  yonedalem3  18248  xpsmnd0  18712  xpsinv  18999  xpsgrpsub  19000  symg2bas  19330  xpsring1d  20249  funcrngcsetc  20556  funcrngcsetcALT  20557  funcringcsetc  20590  rngqiprngimfv  21215  rngqiprngghm  21216  rngqiprngimf1  21217  rngqiprngimfo  21218  rngqiprnglin  21219  rngqipring1  21233  rngqiprngfu  21234  pzriprnglem6  21403  pzriprnglem12  21409  mat1dimmul  22370  txcnp  23514  upxp  23517  uptx  23519  hauseqlcld  23540  txlm  23542  txkgen  23546  cnmpt1t  23559  cnmpt2t  23567  txhmeo  23697  flfcnp2  23901  ucnimalem  24174  ucnima  24175  fmucndlem  24185  fmucnd  24186  cnheiborlem  24860  pi1xfrcnvlem  24963  ovollb2lem  25396  ovollb2  25397  ovolshftlem2  25418  ovolscalem2  25422  ioombl1  25470  ioorf  25481  ioorval  25482  ioorinv2  25483  uniioombllem6  25496  dyadval  25500  opnmbl  25510  mbfimaopnlem  25563  limccnp2  25800  mpodvdsmulf1o  27111  dvdsmulf1o  27113  precsexlemcbv  28115  precsexlem3  28118  seqseq123d  28187  om2noseqrdg  28205  noseqrdgsuc  28209  ebtwntg  28916  numclwwlk1lem2fv  30292  numclwwlk1lem2fo  30294  numclwwlk1lem2  30296  wlkl0  30303  hhssnvt  31201  hhsssh  31205  opsbc2ie  32412  opreu2reuALT  32413  opfv  32575  xppreima  32576  2ndresdju  32580  aciunf1lem  32593  ofpreima  32596  fgreu  32603  gsumwrd2dccatlem  33013  gsumwrd2dccat  33014  rlocval  33217  rlocaddval  33226  rlocmulval  33227  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  zringfrac  33532  smatlem  33794  qtophaus  33833  qqhval2  33979  esum2dlem  34089  rrvadd  34450  hgt750lemb  34654  bnj1442  35046  bnj1450  35047  bnj1463  35052  bnj1529  35067  swrdrevpfx  35111  erdszelem9  35193  erdszelem10  35194  txpconn  35226  txsconnlem  35234  goaleq12d  35345  msubval  35519  msubco  35525  mvhval  35528  msubvrs  35554  cbvoprab123vw  36234  cbvoprab23vw  36235  cbvoprab13vw  36236  cbvopabdavw  36261  cbvoprab123davw  36269  cbvoprab12davw  36270  cbvoprab23davw  36271  cbvoprab13davw  36272  bj-dfid2ALT  37060  bj-endval  37310  finxpreclem3  37388  poimirlem4  37625  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  heiborlem6  37817  heiborlem7  37818  heiborlem8  37819  nfopdALT  38971  dvhvaddcbv  41090  dvhvaddval  41091  dvhopvadd  41094  dvhvaddcomN  41097  dvhvaddass  41098  dvhvscacbv  41099  dvhvscaval  41100  dvhopvsca  41103  dvhgrp  41108  dvhlveclem  41109  dvh0g  41112  dvhopaddN  41115  dvhopspN  41116  dvhopN  41117  cdlemn4  41199  hdmapffval  41827  pellexlem3  42826  pellex  42830  elcnvlem  43597  dvnprodlem1  45951  dvnprodlem3  45953  etransclem44  46283  ovolval4  46656  ovolval5lem3  46659  aoveq123d  47183  prproropf1olem2  47509  prproropf1olem3  47510  prproropf1olem4  47511  prproropf1o  47512  prproropreud  47514  isisubgr  47866  eloprab1st2nd  48860  ssccatid  49065  oppfvalg  49119  imaf1co  49148  uptrlem1  49203  xpcfucco3  49251  dfswapf2  49254  swapfval  49255  swapfcoa  49274  1stfpropd  49283  2ndfpropd  49284  tposcurf1  49292  diag1  49297  fuco2eld2  49307  fucofvalg  49311  fuco21  49329  fuco11bALT  49331  fuco23  49334  fuco22natlem3  49337  fuco22nat  49339  fucoid  49341  fuco22a  49343  fucocolem2  49347  fucocolem4  49349  postcofval  49357  precofval  49360  precofvalALT  49361  precofval3  49364  prcofvalg  49369  prcofpropd  49372  prcofdiag1  49386  prcofdiag  49387  fucoppcco  49402  oppfdiag1  49407  oppfdiag  49409  termcfuncval  49525  diag1f1olem  49526  mndtcval  49572  mndtcco  49578  2arwcatlem2  49589  2arwcatlem3  49590  2arwcatlem4  49591  2arwcat  49593  setc1onsubc  49595  lanfval  49606  ranfval  49607  ranup  49635  concom  49656  islmd  49658