Theorem eceq1 8685

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4582   “ cima 5635  [cec 8643

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-ec 8647

This theorem is referenced by:  eceq1d  8686  ecelqs  8716  snecg  8726  snec  8727  qliftfun  8751  qliftfuns  8753  qliftval  8755  ecoptocl  8756  eroveu  8761  erov  8763  divsfval  17480  qusghm  19196  sylow1lem3  19541  efgi2  19666  frgpup3lem  19718  rngqiprngimfv  21265  rngqiprngimf1  21267  rngqiprngimfo  21268  pzriprnglem11  21458  znzrhval  21513  qustgpopn  24076  qustgplem  24077  elpi1i  25014  pi1xfrf  25021  pi1xfrval  25022  pi1xfrcnvlem  25024  pi1cof  25027  pi1coval  25028  vitalilem3  25579  tgjustr  28558  qusker  33441  qusvscpbl  33443  qusvsval  33444  algextdeg  33902  eceq1i  38532  disjressuc2  38659  ecqmap  38697  disjimeceqim2  39053  disjimeceqbi  39054  disjimeceqbi2  39055  disjimrmoeqec  39056  qmapeldisjsbi  39109  disjlem14  39149  prtlem9  39237  prtlem11  39239  aks6d1c6lem5  42544  aks5lem3a  42556