Theorem eceq1 8722

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

Syntax hints:   → wi 4   = wceq 1563  {csn 4585   “ cima 5654  [cec 8680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ec 8684

This theorem is referenced by:  eceq1d  8723  ecelqs  8753  snecg  8763  snec  8764  qliftfun  8788  qliftfuns  8790  qliftval  8792  ecoptocl  8793  eroveu  8798  erov  8800  divsfval  17589  qusghm  19313  sylow1lem3  19658  efgi2  19783  frgpup3lem  19835  rngqiprngimfv  21397  rngqiprngimf1  21399  rngqiprngimfo  21400  pzriprnglem11  21598  znzrhval  21653  qustgpopn  24234  qustgplem  24235  elpi1i  25162  pi1xfrf  25169  pi1xfrval  25170  pi1xfrcnvlem  25172  pi1cof  25175  pi1coval  25176  vitalilem3  25726  tgjustr  28697  qusker  33579  qusvscpbl  33581  qusvsval  33582  algextdeg  34027  eceq1i  38790  disjressuc2  38917  ecqmap  38955  disjimeceqim2  39311  disjimeceqbi  39312  disjimeceqbi2  39313  disjimrmoeqec  39314  qmapeldisjsbi  39367  disjlem14  39407  prtlem9  39495  prtlem11  39497  aks6d1c6lem5  42801  aks5lem3a  42813