Theorem eceq1 8782

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

Syntax hints:   → wi 4   = wceq 1536  {csn 4630   “ cima 5691  [cec 8741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ec 8745

This theorem is referenced by:  eceq1d  8783  ecelqsg  8810  snec  8818  qliftfun  8840  qliftfuns  8842  qliftval  8844  ecoptocl  8845  eroveu  8850  erov  8852  divsfval  17593  qusghm  19285  sylow1lem3  19632  efgi2  19757  frgpup3lem  19809  rngqiprngimfv  21325  rngqiprngimf1  21327  rngqiprngimfo  21328  pzriprnglem11  21519  znzrhval  21582  qustgpopn  24143  qustgplem  24144  elpi1i  25092  pi1xfrf  25099  pi1xfrval  25100  pi1xfrcnvlem  25102  pi1cof  25105  pi1coval  25106  vitalilem3  25658  tgjustr  28496  qusker  33356  qusvscpbl  33358  qusvsval  33359  algextdeg  33730  eceq1i  38257  disjressuc2  38369  disjlem14  38779  prtlem9  38845  prtlem11  38847  aks6d1c6lem5  42158  aks5lem3a  42170