Theorem eceq1 8310

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

Syntax hints:   → wi 4   = wceq 1538  {csn 4525   “ cima 5522  [cec 8270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ec 8274

This theorem is referenced by:  eceq1d  8311  ecelqsg  8335  snec  8343  qliftfun  8365  qliftfuns  8367  qliftval  8369  ecoptocl  8370  eroveu  8375  erov  8377  divsfval  16812  qusghm  18387  sylow1lem3  18717  efgi2  18843  frgpup3lem  18895  znzrhval  20238  qustgpopn  22725  qustgplem  22726  elpi1i  23651  pi1xfrf  23658  pi1xfrval  23659  pi1xfrcnvlem  23661  pi1cof  23664  pi1coval  23665  vitalilem3  24214  tgjustr  26268  qusker  30969  qusvscpbl  30971  qusscaval  30972  eceq1i  35693  prtlem9  36160  prtlem11  36162