Theorem eceq1 8711

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

Syntax hints:   → wi 4   = wceq 1559  {csn 4579   “ cima 5646  [cec 8669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-ec 8673

This theorem is referenced by:  eceq1d  8712  ecelqs  8742  snecg  8752  snec  8753  qliftfun  8777  qliftfuns  8779  qliftval  8781  ecoptocl  8782  eroveu  8787  erov  8789  divsfval  17567  qusghm  19285  sylow1lem3  19630  efgi2  19755  frgpup3lem  19807  rngqiprngimfv  21355  rngqiprngimf1  21357  rngqiprngimfo  21358  pzriprnglem11  21530  znzrhval  21585  qustgpopn  24167  qustgplem  24168  elpi1i  25095  pi1xfrf  25102  pi1xfrval  25103  pi1xfrcnvlem  25105  pi1cof  25108  pi1coval  25109  vitalilem3  25659  tgjustr  28630  qusker  33495  qusvscpbl  33497  qusvsval  33498  algextdeg  33982  eceq1i  38743  disjressuc2  38870  ecqmap  38908  disjimeceqim2  39264  disjimeceqbi  39265  disjimeceqbi2  39266  disjimrmoeqec  39267  qmapeldisjsbi  39320  disjlem14  39360  prtlem9  39448  prtlem11  39450  aks6d1c6lem5  42754  aks5lem3a  42766