Theorem eceq1 8788

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4588   “ cima 5659  [cec 8746

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-xp 5662  df-cnv 5664  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-ec 8750

This theorem is used by:  eceq1d  8789  ecelqs  8819  snecg  8829  snec  8830  qliftfun  8854  qliftfuns  8856  qliftval  8858  ecoptocl  8859  eroveu  8864  erov  8866  divsfval  17751  qusghm  19501  sylow1lem3  19847  efgi2  19972  frgpup3lem  20024  rngqiprngimfv  21627  rngqiprngimf1  21629  rngqiprngimfo  21630  pzriprnglem11  21830  znzrhval  21885  qustgpopn  24472  qustgplem  24473  elpi1i  25400  pi1xfrf  25407  pi1xfrval  25408  pi1xfrcnvlem  25410  pi1cof  25413  pi1coval  25414  vitalilem3  25964  tgjustr  28969  qusker  33994  qusvscpbl  33996  qusvsval  33997  algextdeg  34440  eceq1i  39419  disjressuc2  39546  ecqmap  39584  disjimeceqim2  39940  disjimeceqbi  39941  disjimeceqbi2  39942  disjimrmoeqec  39943  qmapeldisjsbi  39996  disjlem14  40036  prtlem9  40124  prtlem11  40126  aks6d1c6lem5  43430  aks5lem3a  43442