Theorem eceq1 8671

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 6015	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3		df-ec 8634	. 2 ⊢ [𝐴]𝐶 = (𝐶 “ {𝐴})
4		df-ec 8634	. 2 ⊢ [𝐵]𝐶 = (𝐶 “ {𝐵})
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

Syntax hints:   → wi 4   = wceq 1540  {csn 4579   “ cima 5626  [cec 8630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-ec 8634

This theorem is referenced by:  eceq1d  8672  ecelqs  8702  snec  8712  qliftfun  8736  qliftfuns  8738  qliftval  8740  ecoptocl  8741  eroveu  8746  erov  8748  divsfval  17469  qusghm  19152  sylow1lem3  19497  efgi2  19622  frgpup3lem  19674  rngqiprngimfv  21223  rngqiprngimf1  21225  rngqiprngimfo  21226  pzriprnglem11  21416  znzrhval  21471  qustgpopn  24023  qustgplem  24024  elpi1i  24962  pi1xfrf  24969  pi1xfrval  24970  pi1xfrcnvlem  24972  pi1cof  24975  pi1coval  24976  vitalilem3  25527  tgjustr  28437  qusker  33299  qusvscpbl  33301  qusvsval  33302  algextdeg  33694  eceq1i  38254  disjressuc2  38362  disjlem14  38778  prtlem9  38845  prtlem11  38847  aks6d1c6lem5  42153  aks5lem3a  42165