Theorem opeq2d 4812

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576

This theorem is referenced by:  funopsn  6912  fmptsng  6932  fmptsnd  6933  fvproj  7830  tfrlem11  8026  seqomlem0  8087  seqomlem1  8088  seqomlem4  8091  seqomeq12  8092  fundmen  8585  unxpdomlem1  8724  mulcanenq  10384  elreal2  10556  om2uzrdg  13327  uzrdgsuci  13331  seqeq2  13376  seqeq3  13377  s1val  13954  s1eq  13956  swrdlsw  14031  pfxpfx  14072  swrdccat  14099  swrdccat3blem  14103  swrdccat3b  14104  pfxccatin12d  14109  swrds2  14304  swrds2m  14305  swrd2lsw  14316  eucalgval  15928  setsidvald  16516  ressval  16553  ressress  16564  prdsval  16730  imasval  16786  imasaddvallem  16804  xpsfval  16841  xpsval  16845  cidval  16950  iscatd2  16954  oppcval  16985  ismon  17005  rescval  17099  idfucl  17153  funcres  17168  fucval  17230  fucpropd  17249  setcval  17339  catcval  17358  estrcval  17376  xpcval  17429  1stfcl  17449  2ndfcl  17450  curf12  17479  curf2val  17482  curfcl  17484  hofcl  17511  oduval  17742  ipoval  17766  frmdval  18018  efmnd  18037  oppgval  18477  symgvalstruct  18527  efgmval  18840  efgmnvl  18842  efgi  18847  frgpup3lem  18905  dprd2da  19166  dmdprdpr  19173  dprdpr  19174  pgpfaclem1  19205  mgpval  19244  mgpress  19252  opprval  19376  sraval  19950  rlmval2  19968  psrval  20144  opsrval  20257  opsrval2  20259  zlmval  20665  znval  20684  znval2  20686  thlval  20841  islindf4  20984  matval  21022  mat1dimmul  21087  mat1dimcrng  21088  mat1scmat  21150  mdet0pr  21203  m1detdiag  21208  txkgen  22262  pt1hmeo  22416  xpstopnlem1  22419  xpstopnlem2  22421  tusval  22877  tmsval  23093  tngval  23250  om1val  23636  pi1xfrcnvlem  23662  pi1xfrcnv  23663  dchrval  25812  ttgval  26663  eengv  26767  uspgr1ewop  27032  usgr2v1e2w  27036  1loopgruspgr  27284  1egrvtxdg1r  27294  1egrvtxdg0  27295  eupth2lem3lem3  28011  eupth2  28020  wlkl0  28148  br8d  30363  resvval  30902  smatfval  31062  smatrcl  31063  smatlem  31064  qqhval  31217  bnj66  32134  bnj1234  32287  bnj1296  32295  bnj1450  32324  bnj1463  32329  bnj1501  32341  bnj1523  32345  subfacp1lem5  32433  cvmliftlem10  32543  cvmlift2lem12  32563  goaleq12d  32600  sategoelfvb  32668  msubffval  32772  msubfval  32773  elmsubrn  32777  msubrn  32778  msubco  32780  br8  32994  br6  32995  nosupbnd2lem1  33217  btwnouttr2  33485  brfs  33542  btwnconn1lem11  33560  bj-endval  34598  csbfinxpg  34671  finixpnum  34879  ldualset  36263  tgrpfset  37882  tgrpset  37883  erngfset  37937  erngset  37938  erngfset-rN  37945  erngset-rN  37946  dvafset  38142  dvaset  38143  dvhfset  38218  dvhset  38219  dvhfvadd  38229  dvhopvadd2  38232  dib1dim2  38306  dicvscacl  38329  cdlemn6  38340  dihopelvalcpre  38386  dih1dimatlem  38467  hdmapfval  38965  hlhilset  39072  mendval  39790  ovolval4lem1  42938  ovolval4lem2  42939  ovnovollem3  42947  idfusubc0  44143  idfusubc  44144  rngcvalALTV  44239  ringcvalALTV  44285  zlmodzxzsub  44415  lmod1zr  44555