Theorem eceq1 8761

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {csn 4584   “ cima 5653  [cec 8719

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-ec 8723

This theorem is used by:  eceq1d  8762  ecelqs  8792  snecg  8802  snec  8803  qliftfun  8827  qliftfuns  8829  qliftval  8831  ecoptocl  8832  eroveu  8837  erov  8839  divsfval  17725  qusghm  19475  sylow1lem3  19820  efgi2  19945  frgpup3lem  19997  rngqiprngimfv  21600  rngqiprngimf1  21602  rngqiprngimfo  21603  pzriprnglem11  21803  znzrhval  21858  qustgpopn  24445  qustgplem  24446  elpi1i  25373  pi1xfrf  25380  pi1xfrval  25381  pi1xfrcnvlem  25383  pi1cof  25386  pi1coval  25387  vitalilem3  25937  tgjustr  28942  qusker  33957  qusvscpbl  33959  qusvsval  33960  algextdeg  34404  eceq1i  39310  disjressuc2  39437  ecqmap  39475  disjimeceqim2  39831  disjimeceqbi  39832  disjimeceqbi2  39833  disjimrmoeqec  39834  qmapeldisjsbi  39887  disjlem14  39927  prtlem9  40015  prtlem11  40017  aks6d1c6lem5  43321  aks5lem3a  43333