Theorem eceq1 8667

Description: Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.)

Assertion

Ref	Expression
eceq1	⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Proof of Theorem eceq1

Step	Hyp	Ref	Expression
1		sneq 4585	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	imaeq2d 6013	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3		df-ec 8630	. 2 ⊢ [𝐴]𝐶 = (𝐶 “ {𝐴})
4		df-ec 8630	. 2 ⊢ [𝐵]𝐶 = (𝐶 “ {𝐵})
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1541  {csn 4575   “ cima 5622  [cec 8626

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ec 8630

This theorem is referenced by:  eceq1d  8668  ecelqs  8698  snec  8708  qliftfun  8732  qliftfuns  8734  qliftval  8736  ecoptocl  8737  eroveu  8742  erov  8744  divsfval  17453  qusghm  19169  sylow1lem3  19514  efgi2  19639  frgpup3lem  19691  rngqiprngimfv  21237  rngqiprngimf1  21239  rngqiprngimfo  21240  pzriprnglem11  21430  znzrhval  21485  qustgpopn  24036  qustgplem  24037  elpi1i  24974  pi1xfrf  24981  pi1xfrval  24982  pi1xfrcnvlem  24984  pi1cof  24987  pi1coval  24988  vitalilem3  25539  tgjustr  28453  qusker  33321  qusvscpbl  33323  qusvsval  33324  algextdeg  33759  eceq1i  38337  disjressuc2  38456  disjlem14  38917  prtlem9  38984  prtlem11  38986  aks6d1c6lem5  42291  aks5lem3a  42303