Theorem opeq2d 4838

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 4832	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  dfid2  5529  funopsn  7103  fmptsng  7124  fmptsnd  7125  fvproj  8086  tfrlem11  8329  seqomlem0  8390  seqomlem1  8391  seqomlem4  8394  seqomeq12  8395  fundmen  8980  dif1en  9098  unxpdomlem1  9168  mulcanenq  10883  elreal2  11055  om2uzrdg  13891  uzrdgsuci  13895  seqeq2  13940  seqeq3  13941  s1val  14534  s1eq  14536  swrdlsw  14603  pfxpfx  14643  swrdccat  14670  swrdccat3blem  14674  swrdccat3b  14675  pfxccatin12d  14680  swrds2  14875  swrds2m  14876  swrd2lsw  14887  eucalgval  16521  setsidvald  17138  ressval  17172  ressress  17186  prdsval  17387  imasval  17444  imasaddvallem  17462  xpsfval  17499  xpsval  17503  cidval  17612  iscatd2  17616  oppcval  17648  ismon  17669  rescval  17763  idfucl  17817  funcres  17832  idfusubc0  17835  idfusubc  17836  fucval  17897  fucpropd  17916  setcval  18013  catcval  18036  estrcval  18059  xpcval  18112  1stfcl  18132  2ndfcl  18133  curf12  18162  curf2val  18165  curfcl  18167  hofcl  18194  oduval  18223  ipoval  18465  frmdval  18788  efmnd  18807  oppgval  19288  symgvalstruct  19338  efgmval  19653  efgmnvl  19655  efgi  19660  frgpup3lem  19718  dprd2da  19985  dmdprdpr  19992  dprdpr  19993  pgpfaclem1  20024  mgpval  20090  mgpress  20097  opprval  20286  sraval  21139  rlmval2  21156  pzriprnglem10  21457  zlmval  21482  znval  21502  znval2  21504  thlval  21662  islindf4  21805  psrval  21883  opsrval  22013  opsrval2  22015  matval  22367  mat1dimmul  22432  mat1dimcrng  22433  mat1scmat  22495  mdet0pr  22548  m1detdiag  22553  txkgen  23608  pt1hmeo  23762  xpstopnlem1  23765  xpstopnlem2  23767  tusval  24221  tmsval  24437  tngval  24595  om1val  24998  pi1xfrcnvlem  25024  pi1xfrcnv  25025  dchrval  27213  nosupbnd2lem1  27695  noinfbnd2lem1  27710  seqseq123d  28294  om2noseqrdg  28312  noseqrdgsuc  28316  ttgval  28959  eengv  29064  uspgr1ewop  29333  usgr2v1e2w  29337  1loopgruspgr  29586  1egrvtxdg1r  29596  1egrvtxdg0  29597  eupth2lem3lem3  30317  eupth2  30326  wlkl0  30454  br8d  32697  fresunsn  32714  elrgspnlem2  33336  rlocval  33352  rlocf1  33366  resvval  33421  opprabs  33574  idlsrgval  33595  extvfvcl  33712  resssra  33763  smatfval  33972  smatrcl  33973  smatlem  33974  qqhval  34149  bnj66  35035  bnj1234  35188  bnj1296  35196  bnj1450  35225  bnj1463  35230  bnj1501  35242  bnj1523  35246  subfacp1lem5  35397  cvmliftlem10  35507  cvmlift2lem12  35527  goaleq12d  35564  sategoelfvb  35632  msubffval  35736  msubfval  35737  elmsubrn  35741  msubrn  35742  msubco  35744  br8  35969  br6  35970  btwnouttr2  36235  brfs  36292  btwnconn1lem11  36310  cbvoprab3davw  36486  bj-dfid2ALT  37310  bj-endval  37567  csbfinxpg  37640  finixpnum  37853  ldualset  39498  tgrpfset  41117  tgrpset  41118  erngfset  41172  erngset  41173  erngfset-rN  41180  erngset-rN  41181  dvafset  41377  dvaset  41378  dvhfset  41453  dvhset  41454  dvhfvadd  41464  dvhopvadd2  41467  dib1dim2  41541  dicvscacl  41564  cdlemn6  41575  dihopelvalcpre  41621  dih1dimatlem  41702  hdmapfval  42200  hlhilset  42307  mendval  43533  mnringvald  44566  ovolval4lem1  47004  ovolval4lem2  47005  ovnovollem3  47013  isubgrvtxuhgr  48221  isubgr0uhgr  48230  stgrfv  48310  gpgov  48399  gpgprismgriedgdmss  48409  gpgvtx0  48410  gpgvtx1  48411  gpgedgvtx0  48418  gpgedgvtx1  48419  gpgvtxedg0  48420  gpgvtxedg1  48421  gpgedgiov  48422  gpgedg2ov  48423  gpgedg2iv  48424  gpg3kgrtriexlem6  48445  gpg3kgrtriex  48446  gpgprismgr4cycllem3  48454  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2  48474  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5  48480  gpg5edgnedg  48487  rngcvalALTV  48622  ringcvalALTV  48646  zlmodzxzsub  48717  lmod1zr  48850  2arymaptf  49009  discsubc  49420  2oppf  49488  upfval2  49533  upfval3  49534  isuplem  49535  uptpos  49554  uptr2  49577  dfswapf2  49617  oppc1stf  49644  oppc2ndf  49645  fucolid  49717  fucorid  49718  precofval2  49725  prcofval  49734  isinito2lem  49854  termcfuncval  49888  prstcval  49907  mndtcval  49935  lanup  49997  coccom  50020  iscmd  50022