Theorem opeq12d 4851

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4600

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is used by:  nfopd  4860  moop2  5490  iunopeqop  5509  iunopeqopOLD  5510  dfid2  5563  fsn2g  7141  funopsn  7151  funopsnOLD  7152  fnprb  7213  fntpb  7214  fnpr2g  7215  fliftfuns  7323  dfmpo  8106  fsplit  8121  fsplitfpar  8122  fnwelem  8136  fimaproj  8140  seqomlem0  8445  seqomlem1  8446  seqomlem4  8449  qliftfuns  8811  xpassen  9069  xpdom2  9070  xpf1o  9137  xpmapenlem  9142  xpmapen  9143  mapunen  9144  xpwdomg  9557  fseqenlem2  10028  nqereu  10932  addpipq2  10939  addpipq  10940  mulpipq2  10942  mulpipq  10943  1nqenq  10965  mulidnq  10966  ltexnq  10978  prlem934  11036  addsrmo  11076  mulsrmo  11077  addsrpr  11078  mulsrpr  11079  mulcnsr  11139  mulresr  11142  axcnre  11167  om2uzrdg  14012  uzrdgsuci  14016  pfxsuff1eqwrdeq  14760  swrdpfx  14768  ccatopth  14777  swrdccatin2d  14805  splval  14812  splcl  14813  swrdrevpfx  14830  cshfn  14853  repswcshw  14875  2swrd2eqwrdeq  15016  ruclem1  16312  eucalgval2  16664  qnumdenbi  16828  crth  16862  phimullem  16863  prmreclem3  17003  setsstruct  17261  ressval3d  17331  imasval  17590  imasaddvallem  17608  xpsff1o  17646  catidex  17755  cidval  17758  catcocl  17766  catass  17767  oppccofval  17797  sectfval  17833  subccocl  17927  isfunc  17946  funcco  17953  idfuval  17958  idfucl  17963  cofuval  17964  cofuval2  17969  cofucl  17970  cofuass  17971  cofulid  17972  cofurid  17973  resfval  17974  resfval2  17975  funcres  17978  inclfusubc  18025  isnat  18032  nati  18040  fucco  18047  fuccoval  18048  coaval  18150  catcisolem  18192  xpcval  18258  xpcco  18264  xpcco2  18268  xpccatid  18269  xpcid  18270  1stfval  18272  2ndfval  18275  1stfcl  18278  2ndfcl  18279  prfval  18280  prf1  18281  prf2fval  18282  prf2  18283  prfcl  18284  prf1st  18285  prf2nd  18286  1st2ndprf  18287  xpcpropd  18289  evlfval  18298  evlf2  18299  evlfcllem  18302  evlfcl  18303  curfval  18304  curf1  18306  curf1cl  18309  curf2cl  18312  curfcl  18313  curfpropd  18314  uncf1  18317  uncf2  18318  curfuncf  18319  uncfcurf  18320  diagval  18321  curf2ndf  18328  hofval  18333  hof2fval  18336  hofcl  18340  yonval  18342  hofpropd  18348  yonedalem21  18354  yonedalem22  18359  yonedalem3  18361  xpsmnd0  18867  xpsinv  19157  xpsgrpsub  19158  symg2bas  19494  xpsring1d  20448  funcrngcsetc  20776  funcrngcsetcALT  20777  funcringcsetc  20810  rngqiprngimfv  21475  rngqiprngghm  21476  rngqiprngimf1  21477  rngqiprngimfo  21478  rngqiprnglin  21479  rngqipring1  21493  rngqiprngfu  21494  pzriprnglem6  21673  pzriprnglem12  21679  mat1dimmul  22670  txcnp  23814  upxp  23817  uptx  23819  hauseqlcld  23840  txlm  23842  txkgen  23846  cnmpt1t  23859  cnmpt2t  23867  txhmeo  23997  flfcnp2  24201  ucnimalem  24473  ucnima  24474  fmucndlem  24484  fmucnd  24485  cnheiborlem  25150  pi1xfrcnvlem  25252  ovollb2lem  25684  ovollb2  25685  ovolshftlem2  25706  ovolscalem2  25710  ioombl1  25758  ioorf  25769  ioorval  25770  ioorinv2  25771  uniioombllem6  25784  dyadval  25788  opnmbl  25798  mbfimaopnlem  25851  limccnp2  26088  mpodvdsmulf1o  27395  dvdsmulf1o  27397  precsexlemcbv  28436  precsexlem3  28439  seqseq123d  28516  om2noseqrdg  28534  noseqrdgsuc  28538  ebtwntg  29369  numclwwlk1lem2fv  30744  numclwwlk1lem2fo  30746  numclwwlk1lem2  30748  wlkl0  30755  hhssnvt  31654  hhsssh  31658  opsbc2ie  32859  opreu2reuALT  32860  opfv  33026  xppreima  33027  2ndresdju  33031  aciunf1lem  33044  ofpreima  33047  fgreu  33053  gsumwrd2dccatlem  33428  gsumwrd2dccat  33429  rlocval  33610  rlocaddval  33620  rlocmulval  33621  rloccring  33622  rloc0g  33623  rloc1r  33624  rlocf1  33625  rlocinvunit  33626  rlocisunit  33627  zringfrac  33875  smatlem  34218  qtophaus  34257  qqhval2  34403  esum2dlem  34513  rrvadd  34874  hgt750lemb  35075  bnj1442  35469  bnj1450  35470  bnj1463  35475  bnj1529  35490  erdszelem9  35712  erdszelem10  35713  txpconn  35745  txsconnlem  35753  goaleq12d  35864  msubval  36038  msubco  36044  mvhval  36047  msubvrs  36073  cbvoprab123vw  36792  cbvoprab23vw  36793  cbvoprab13vw  36794  cbvopabdavw  36819  cbvoprab123davw  36827  cbvoprab12davw  36828  cbvoprab23davw  36829  cbvoprab13davw  36830  bj-dfid2ALT  37742  bj-endval  38000  finxpreclem3  38080  poimirlem4  38316  opnmbllem0  38348  mblfinlem1  38349  mblfinlem2  38350  heiborlem6  38508  heiborlem7  38509  heiborlem8  38510  nfopdALT  39786  dvhvaddcbv  41904  dvhvaddval  41905  dvhopvadd  41908  dvhvaddcomN  41911  dvhvaddass  41912  dvhvscacbv  41913  dvhvscaval  41914  dvhopvsca  41917  dvhgrp  41922  dvhlveclem  41923  dvh0g  41926  dvhopaddN  41929  dvhopspN  41930  dvhopN  41931  cdlemn4  42013  hdmapffval  42641  pellexlem3  43599  pellex  43603  elcnvlem  44368  dvnprodlem1  46701  dvnprodlem3  46703  etransclem44  47033  ovolval4  47406  ovolval5lem3  47409  aoveq123d  47956  prproropf1olem2  48294  prproropf1olem3  48295  prproropf1olem4  48296  prproropf1o  48297  prproropreud  48299  isisubgr  48668  eloprab1st2nd  49687  ssccatid  49891  oppfvalg  49945  imaf1co  49974  uptrlem1  50029  xpcfucco3  50077  dfswapf2  50080  swapfval  50081  swapfcoa  50100  1stfpropd  50109  2ndfpropd  50110  tposcurf1  50118  diag1  50123  fuco2eld2  50133  fucofvalg  50137  fuco21  50155  fuco11bALT  50157  fuco23  50160  fuco22natlem3  50163  fuco22nat  50165  fucoid  50167  fuco22a  50169  fucocolem2  50173  fucocolem4  50175  postcofval  50183  precofval  50186  precofvalALT  50187  precofval3  50190  prcofvalg  50195  prcofpropd  50198  prcofdiag1  50212  prcofdiag  50213  fucoppcco  50228  oppfdiag1  50233  oppfdiag  50235  termcfuncval  50351  diag1f1olem  50352  mndtcval  50398  mndtcco  50404  2arwcatlem2  50415  2arwcatlem3  50416  2arwcatlem4  50417  2arwcat  50419  setc1onsubc  50421  lanfval  50432  ranfval  50433  ranup  50461  concom  50482  islmd  50484