Theorem eceq1 8784

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 4636	. . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
2	1	imaeq2d 6078	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3		df-ec 8747	. 2 ⊢ [𝐴]𝐶 = (𝐶 “ {𝐴})
4		df-ec 8747	. 2 ⊢ [𝐵]𝐶 = (𝐶 “ {𝐵})
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1540  {csn 4626   “ cima 5688  [cec 8743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ec 8747

This theorem is referenced by:  eceq1d  8785  ecelqsg  8812  snec  8820  qliftfun  8842  qliftfuns  8844  qliftval  8846  ecoptocl  8847  eroveu  8852  erov  8854  divsfval  17592  qusghm  19273  sylow1lem3  19618  efgi2  19743  frgpup3lem  19795  rngqiprngimfv  21308  rngqiprngimf1  21310  rngqiprngimfo  21311  pzriprnglem11  21502  znzrhval  21565  qustgpopn  24128  qustgplem  24129  elpi1i  25079  pi1xfrf  25086  pi1xfrval  25087  pi1xfrcnvlem  25089  pi1cof  25092  pi1coval  25093  vitalilem3  25645  tgjustr  28482  qusker  33377  qusvscpbl  33379  qusvsval  33380  algextdeg  33766  eceq1i  38277  disjressuc2  38389  disjlem14  38799  prtlem9  38865  prtlem11  38867  aks6d1c6lem5  42178  aks5lem3a  42190