Theorem eceq1 8736

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

Syntax hints:   → wi 4   = wceq 1567  {csn 4594   “ cima 5667  [cec 8694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5670  df-cnv 5672  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-ec 8698

This theorem is referenced by:  eceq1d  8737  ecelqs  8767  snecg  8777  snec  8778  qliftfun  8802  qliftfuns  8804  qliftval  8806  ecoptocl  8807  eroveu  8812  erov  8814  divsfval  17603  qusghm  19327  sylow1lem3  19672  efgi2  19797  frgpup3lem  19849  rngqiprngimfv  21411  rngqiprngimf1  21413  rngqiprngimfo  21414  pzriprnglem11  21612  znzrhval  21667  qustgpopn  24248  qustgplem  24249  elpi1i  25176  pi1xfrf  25183  pi1xfrval  25184  pi1xfrcnvlem  25186  pi1cof  25189  pi1coval  25190  vitalilem3  25740  tgjustr  28711  qusker  33614  qusvscpbl  33616  qusvsval  33617  algextdeg  34062  eceq1i  38860  disjressuc2  38987  ecqmap  39025  disjimeceqim2  39381  disjimeceqbi  39382  disjimeceqbi2  39383  disjimrmoeqec  39384  qmapeldisjsbi  39437  disjlem14  39477  prtlem9  39565  prtlem11  39567  aks6d1c6lem5  42871  aks5lem3a  42883