Theorem opeq12d 4905

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  nfopd  4914  moop2  5521  iunopeqop  5540  dfid2  5595  fsn2g  7172  funopsn  7182  fnprb  7245  fntpb  7246  fnpr2g  7247  fliftfuns  7350  dfmpo  8143  fsplit  8158  fsplitfpar  8159  fnwelem  8172  fimaproj  8176  seqomlem0  8505  seqomlem1  8506  seqomlem4  8509  qliftfuns  8862  xpassen  9132  xpdom2  9133  xpf1o  9205  xpmapenlem  9210  xpmapen  9211  mapunen  9212  xpwdomg  9654  fseqenlem2  10094  nqereu  10998  addpipq2  11005  addpipq  11006  mulpipq2  11008  mulpipq  11009  1nqenq  11031  mulidnq  11032  ltexnq  11044  prlem934  11102  addsrmo  11142  mulsrmo  11143  addsrpr  11144  mulsrpr  11145  mulcnsr  11205  mulresr  11208  axcnre  11233  om2uzrdg  14007  uzrdgsuci  14011  pfxsuff1eqwrdeq  14747  swrdpfx  14755  ccatopth  14764  swrdccatin2d  14792  splval  14799  splcl  14800  cshfn  14838  repswcshw  14860  2swrd2eqwrdeq  15002  ruclem1  16279  eucalgval2  16628  qnumdenbi  16791  crth  16825  phimullem  16826  prmreclem3  16965  setsstruct  17223  ressval3d  17305  ressval3dOLD  17306  imasval  17571  imasaddvallem  17589  xpsff1o  17627  catidex  17732  cidval  17735  catcocl  17743  catass  17744  oppccofval  17775  sectfval  17812  subccocl  17909  isfunc  17928  funcco  17935  idfuval  17940  idfucl  17945  cofuval  17946  cofuval2  17951  cofucl  17952  cofuass  17953  cofulid  17954  cofurid  17955  resfval  17956  resfval2  17957  funcres  17960  inclfusubc  18008  isnat  18015  nati  18023  fucco  18032  fuccoval  18033  coaval  18135  catcisolem  18177  xpcval  18246  xpcco  18252  xpcco2  18256  xpccatid  18257  xpcid  18258  1stfval  18260  2ndfval  18263  1stfcl  18266  2ndfcl  18267  prfval  18268  prf1  18269  prf2fval  18270  prf2  18271  prfcl  18272  prf1st  18273  prf2nd  18274  1st2ndprf  18275  xpcpropd  18278  evlfval  18287  evlf2  18288  evlfcllem  18291  evlfcl  18292  curfval  18293  curf1  18295  curf1cl  18298  curf2cl  18301  curfcl  18302  curfpropd  18303  uncf1  18306  uncf2  18307  curfuncf  18308  uncfcurf  18309  diagval  18310  curf2ndf  18317  hofval  18322  hof2fval  18325  hofcl  18329  yonval  18331  hofpropd  18337  yonedalem21  18343  yonedalem22  18348  yonedalem3  18350  xpsmnd0  18813  xpsinv  19100  xpsgrpsub  19101  symg2bas  19434  xpsring1d  20356  funcrngcsetc  20662  funcrngcsetcALT  20663  funcringcsetc  20696  rngqiprngimfv  21331  rngqiprngghm  21332  rngqiprngimf1  21333  rngqiprngimfo  21334  rngqiprnglin  21335  rngqipring1  21349  rngqiprngfu  21350  pzriprnglem6  21520  pzriprnglem12  21526  mat1dimmul  22503  txcnp  23649  upxp  23652  uptx  23654  hauseqlcld  23675  txlm  23677  txkgen  23681  cnmpt1t  23694  cnmpt2t  23702  txhmeo  23832  flfcnp2  24036  ucnimalem  24310  ucnima  24311  fmucndlem  24321  fmucnd  24322  cnheiborlem  25005  pi1xfrcnvlem  25108  ovollb2lem  25542  ovollb2  25543  ovolshftlem2  25564  ovolscalem2  25568  ioombl1  25616  ioorf  25627  ioorval  25628  ioorinv2  25629  uniioombllem6  25642  dyadval  25646  opnmbl  25656  mbfimaopnlem  25709  limccnp2  25947  mpodvdsmulf1o  27255  dvdsmulf1o  27257  precsexlemcbv  28248  precsexlem3  28251  seqseq123d  28310  om2noseqrdg  28328  noseqrdgsuc  28332  ebtwntg  29015  numclwwlk1lem2fv  30388  numclwwlk1lem2fo  30390  numclwwlk1lem2  30392  wlkl0  30399  hhssnvt  31297  hhsssh  31301  opsbc2ie  32504  opreu2reuALT  32505  opfv  32663  xppreima  32664  2ndresdju  32667  aciunf1lem  32680  ofpreima  32683  fgreu  32690  rlocval  33231  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rloc0g  33243  rloc1r  33244  rlocf1  33245  zringfrac  33547  smatlem  33743  qtophaus  33782  qqhval2  33928  esum2dlem  34056  rrvadd  34417  hgt750lemb  34633  bnj1442  35025  bnj1450  35026  bnj1463  35031  bnj1529  35046  swrdrevpfx  35084  erdszelem9  35167  erdszelem10  35168  txpconn  35200  txsconnlem  35208  goaleq12d  35319  msubval  35493  msubco  35499  mvhval  35502  msubvrs  35528  cbvoprab123vw  36205  cbvoprab23vw  36206  cbvoprab13vw  36207  cbvopabdavw  36232  cbvoprab123davw  36240  cbvoprab12davw  36241  cbvoprab23davw  36242  cbvoprab13davw  36243  bj-dfid2ALT  37031  bj-endval  37281  finxpreclem3  37359  poimirlem4  37584  opnmbllem0  37616  mblfinlem1  37617  mblfinlem2  37618  heiborlem6  37776  heiborlem7  37777  heiborlem8  37778  nfopdALT  38927  dvhvaddcbv  41046  dvhvaddval  41047  dvhopvadd  41050  dvhvaddcomN  41053  dvhvaddass  41054  dvhvscacbv  41055  dvhvscaval  41056  dvhopvsca  41059  dvhgrp  41064  dvhlveclem  41065  dvh0g  41068  dvhopaddN  41071  dvhopspN  41072  dvhopN  41073  cdlemn4  41155  hdmapffval  41783  pellexlem3  42787  pellex  42791  elcnvlem  43563  dvnprodlem1  45867  dvnprodlem3  45869  etransclem44  46199  ovolval4  46572  ovolval5lem3  46575  aoveq123d  47093  prproropf1olem2  47378  prproropf1olem3  47379  prproropf1olem4  47380  prproropf1o  47381  prproropreud  47383  isisubgr  47734  mndtcval  48752  mndtcco  48758