Theorem eceq1 8683

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4567   “ cima 5634  [cec 8641

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ec 8645

This theorem is referenced by:  eceq1d  8684  ecelqs  8714  snecg  8724  snec  8725  qliftfun  8749  qliftfuns  8751  qliftval  8753  ecoptocl  8754  eroveu  8759  erov  8761  divsfval  17511  qusghm  19230  sylow1lem3  19575  efgi2  19700  frgpup3lem  19752  rngqiprngimfv  21296  rngqiprngimf1  21298  rngqiprngimfo  21299  pzriprnglem11  21471  znzrhval  21526  qustgpopn  24085  qustgplem  24086  elpi1i  25013  pi1xfrf  25020  pi1xfrval  25021  pi1xfrcnvlem  25023  pi1cof  25026  pi1coval  25027  vitalilem3  25577  tgjustr  28542  qusker  33409  qusvscpbl  33411  qusvsval  33412  algextdeg  33869  eceq1i  38605  disjressuc2  38732  ecqmap  38770  disjimeceqim2  39126  disjimeceqbi  39127  disjimeceqbi2  39128  disjimrmoeqec  39129  qmapeldisjsbi  39182  disjlem14  39222  prtlem9  39310  prtlem11  39312  aks6d1c6lem5  42616  aks5lem3a  42628