Theorem opeq2d 4823

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  dfid2  5528  funopsn  7101  funopsnOLD  7102  fmptsng  7123  fmptsnd  7124  fvproj  8084  tfrlem11  8327  seqomlem0  8388  seqomlem1  8389  seqomlem4  8392  seqomeq12  8393  fundmen  8978  dif1en  9096  unxpdomlem1  9166  mulcanenq  10883  elreal2  11055  om2uzrdg  13918  uzrdgsuci  13922  seqeq2  13967  seqeq3  13968  s1val  14561  s1eq  14563  swrdlsw  14630  pfxpfx  14670  swrdccat  14697  swrdccat3blem  14701  swrdccat3b  14702  pfxccatin12d  14707  swrds2  14902  swrds2m  14903  swrd2lsw  14914  eucalgval  16551  setsidvald  17169  ressval  17203  ressress  17217  prdsval  17418  imasval  17475  imasaddvallem  17493  xpsfval  17530  xpsval  17534  cidval  17643  iscatd2  17647  oppcval  17679  ismon  17700  rescval  17794  idfucl  17848  funcres  17863  idfusubc0  17866  idfusubc  17867  fucval  17928  fucpropd  17947  setcval  18044  catcval  18067  estrcval  18090  xpcval  18143  1stfcl  18163  2ndfcl  18164  curf12  18193  curf2val  18196  curfcl  18198  hofcl  18225  oduval  18254  ipoval  18496  frmdval  18819  efmnd  18838  oppgval  19322  symgvalstruct  19372  efgmval  19687  efgmnvl  19689  efgi  19694  frgpup3lem  19752  dprd2da  20019  dmdprdpr  20026  dprdpr  20027  pgpfaclem1  20058  mgpval  20124  mgpress  20131  opprval  20318  sraval  21170  rlmval2  21187  pzriprnglem10  21470  zlmval  21495  znval  21515  znval2  21517  thlval  21675  islindf4  21818  psrval  21895  opsrval  22024  opsrval2  22026  matval  22376  mat1dimmul  22441  mat1dimcrng  22442  mat1scmat  22504  mdet0pr  22557  m1detdiag  22562  txkgen  23617  pt1hmeo  23771  xpstopnlem1  23774  xpstopnlem2  23776  tusval  24230  tmsval  24446  tngval  24604  om1val  24997  pi1xfrcnvlem  25023  pi1xfrcnv  25024  dchrval  27197  nosupbnd2lem1  27679  noinfbnd2lem1  27694  seqseq123d  28278  om2noseqrdg  28296  noseqrdgsuc  28300  ttgval  28943  eengv  29048  uspgr1ewop  29317  usgr2v1e2w  29321  1loopgruspgr  29569  1egrvtxdg1r  29579  1egrvtxdg0  29580  eupth2lem3lem3  30300  eupth2  30309  wlkl0  30437  br8d  32681  fresunsn  32698  elrgspnlem2  33304  rlocval  33320  rlocf1  33334  resvval  33389  opprabs  33542  idlsrgval  33563  extvfvcl  33680  resssra  33731  smatfval  33939  smatrcl  33940  smatlem  33941  qqhval  34116  bnj66  35002  bnj1234  35155  bnj1296  35163  bnj1450  35192  bnj1463  35197  bnj1501  35209  bnj1523  35213  subfacp1lem5  35366  cvmliftlem10  35476  cvmlift2lem12  35496  goaleq12d  35533  sategoelfvb  35601  msubffval  35705  msubfval  35706  elmsubrn  35710  msubrn  35711  msubco  35713  br8  35938  br6  35939  btwnouttr2  36204  brfs  36261  btwnconn1lem11  36279  cbvoprab3davw  36455  bj-dfid2ALT  37372  bj-endval  37629  csbfinxpg  37704  finixpnum  37926  ldualset  39571  tgrpfset  41190  tgrpset  41191  erngfset  41245  erngset  41246  erngfset-rN  41253  erngset-rN  41254  dvafset  41450  dvaset  41451  dvhfset  41526  dvhset  41527  dvhfvadd  41537  dvhopvadd2  41540  dib1dim2  41614  dicvscacl  41637  cdlemn6  41648  dihopelvalcpre  41694  dih1dimatlem  41775  hdmapfval  42273  hlhilset  42380  mendval  43607  mnringvald  44640  ovolval4lem1  47077  ovolval4lem2  47078  ovnovollem3  47086  isubgrvtxuhgr  48340  isubgr0uhgr  48349  stgrfv  48429  gpgov  48518  gpgprismgriedgdmss  48528  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpg3kgrtriexlem6  48564  gpg3kgrtriex  48565  gpgprismgr4cycllem3  48573  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  gpg5edgnedg  48606  rngcvalALTV  48741  ringcvalALTV  48765  zlmodzxzsub  48836  lmod1zr  48969  2arymaptf  49128  discsubc  49539  2oppf  49607  upfval2  49652  upfval3  49653  isuplem  49654  uptpos  49673  uptr2  49696  dfswapf2  49736  oppc1stf  49763  oppc2ndf  49764  fucolid  49836  fucorid  49837  precofval2  49844  prcofval  49853  isinito2lem  49973  termcfuncval  50007  prstcval  50026  mndtcval  50054  lanup  50116  coccom  50139  iscmd  50141