Theorem eceq1 8676

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4568   “ cima 5627  [cec 8634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ec 8638

This theorem is referenced by:  eceq1d  8677  ecelqs  8707  snecg  8717  snec  8718  qliftfun  8742  qliftfuns  8744  qliftval  8746  ecoptocl  8747  eroveu  8752  erov  8754  divsfval  17502  qusghm  19221  sylow1lem3  19566  efgi2  19691  frgpup3lem  19743  rngqiprngimfv  21288  rngqiprngimf1  21290  rngqiprngimfo  21291  pzriprnglem11  21481  znzrhval  21536  qustgpopn  24095  qustgplem  24096  elpi1i  25023  pi1xfrf  25030  pi1xfrval  25031  pi1xfrcnvlem  25033  pi1cof  25036  pi1coval  25037  vitalilem3  25587  tgjustr  28556  qusker  33424  qusvscpbl  33426  qusvsval  33427  algextdeg  33885  eceq1i  38619  disjressuc2  38746  ecqmap  38784  disjimeceqim2  39140  disjimeceqbi  39141  disjimeceqbi2  39142  disjimrmoeqec  39143  qmapeldisjsbi  39196  disjlem14  39236  prtlem9  39324  prtlem11  39326  aks6d1c6lem5  42630  aks5lem3a  42642