Theorem opeq2d 4881

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq2d	⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq2 4875	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  dfid2  5577  funopsn  7146  fmptsng  7166  fmptsnd  7167  fvproj  8120  tfrlem11  8388  seqomlem0  8449  seqomlem1  8450  seqomlem4  8453  seqomeq12  8454  fundmen  9031  dif1en  9160  dif1enOLD  9162  unxpdomlem1  9250  mulcanenq  10955  elreal2  11127  om2uzrdg  13921  uzrdgsuci  13925  seqeq2  13970  seqeq3  13971  s1val  14548  s1eq  14550  swrdlsw  14617  pfxpfx  14658  swrdccat  14685  swrdccat3blem  14689  swrdccat3b  14690  pfxccatin12d  14695  swrds2  14891  swrds2m  14892  swrd2lsw  14903  eucalgval  16519  setsidvald  17132  setsidvaldOLD  17133  ressval  17176  ressress  17193  prdsval  17401  imasval  17457  imasaddvallem  17475  xpsfval  17512  xpsval  17516  cidval  17621  iscatd2  17625  oppcval  17657  ismon  17680  rescval  17774  idfucl  17831  funcres  17846  fucval  17910  fucpropd  17930  setcval  18027  catcval  18050  estrcval  18075  xpcval  18129  1stfcl  18149  2ndfcl  18150  curf12  18180  curf2val  18183  curfcl  18185  hofcl  18212  oduval  18241  ipoval  18483  frmdval  18732  efmnd  18751  oppgval  19211  symgvalstruct  19264  symgvalstructOLD  19265  efgmval  19580  efgmnvl  19582  efgi  19587  frgpup3lem  19645  dprd2da  19912  dmdprdpr  19919  dprdpr  19920  pgpfaclem1  19951  mgpval  19990  mgpress  20002  mgpressOLD  20003  opprval  20151  sraval  20789  rlmval2  20816  zlmval  21065  znval  21087  znval2  21089  thlval  21248  islindf4  21393  psrval  21468  opsrval  21601  opsrval2  21603  matval  21911  mat1dimmul  21978  mat1dimcrng  21979  mat1scmat  22041  mdet0pr  22094  m1detdiag  22099  txkgen  23156  pt1hmeo  23310  xpstopnlem1  23313  xpstopnlem2  23315  tusval  23770  tmsval  23989  tngval  24148  om1val  24546  pi1xfrcnvlem  24572  pi1xfrcnv  24573  dchrval  26737  nosupbnd2lem1  27218  noinfbnd2lem1  27233  ttgval  28126  ttgvalOLD  28127  eengv  28237  uspgr1ewop  28505  usgr2v1e2w  28509  1loopgruspgr  28757  1egrvtxdg1r  28767  1egrvtxdg0  28768  eupth2lem3lem3  29483  eupth2  29492  wlkl0  29620  br8d  31839  resvval  32441  opprabs  32596  idlsrgval  32617  smatfval  32775  smatrcl  32776  smatlem  32777  qqhval  32954  bnj66  33871  bnj1234  34024  bnj1296  34032  bnj1450  34061  bnj1463  34066  bnj1501  34078  bnj1523  34082  subfacp1lem5  34175  cvmliftlem10  34285  cvmlift2lem12  34305  goaleq12d  34342  sategoelfvb  34410  msubffval  34514  msubfval  34515  elmsubrn  34519  msubrn  34520  msubco  34522  br8  34726  br6  34727  btwnouttr2  34994  brfs  35051  btwnconn1lem11  35069  bj-dfid2ALT  35946  bj-endval  36196  csbfinxpg  36269  finixpnum  36473  ldualset  37995  tgrpfset  39615  tgrpset  39616  erngfset  39670  erngset  39671  erngfset-rN  39678  erngset-rN  39679  dvafset  39875  dvaset  39876  dvhfset  39951  dvhset  39952  dvhfvadd  39962  dvhopvadd2  39965  dib1dim2  40039  dicvscacl  40062  cdlemn6  40073  dihopelvalcpre  40119  dih1dimatlem  40200  hdmapfval  40698  hlhilset  40805  mendval  41925  mnringvald  42967  ovolval4lem1  45365  ovolval4lem2  45366  ovnovollem3  45374  idfusubc0  46639  idfusubc  46640  pzriprnglem10  46814  rngcvalALTV  46859  ringcvalALTV  46905  zlmodzxzsub  47036  lmod1zr  47174  2arymaptf  47338  prstcval  47684  mndtcval  47705