Theorem eceq1 8740

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4587   “ cima 5662  [cec 8698

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-ec 8702

This theorem is used by:  eceq1d  8741  ecelqs  8771  snecg  8781  snec  8782  qliftfun  8806  qliftfuns  8808  qliftval  8810  ecoptocl  8811  eroveu  8816  erov  8818  divsfval  17639  qusghm  19388  sylow1lem3  19733  efgi2  19858  frgpup3lem  19910  rngqiprngimfv  21507  rngqiprngimf1  21509  rngqiprngimfo  21510  pzriprnglem11  21710  znzrhval  21765  qustgpopn  24352  qustgplem  24353  elpi1i  25280  pi1xfrf  25287  pi1xfrval  25288  pi1xfrcnvlem  25290  pi1cof  25293  pi1coval  25294  vitalilem3  25844  tgjustr  28823  qusker  33797  qusvscpbl  33799  qusvsval  33800  algextdeg  34243  eceq1i  39040  disjressuc2  39167  ecqmap  39205  disjimeceqim2  39561  disjimeceqbi  39562  disjimeceqbi2  39563  disjimrmoeqec  39564  qmapeldisjsbi  39617  disjlem14  39657  prtlem9  39745  prtlem11  39747  aks6d1c6lem5  43051  aks5lem3a  43063