Theorem eceq1 8019

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

Syntax hints:   → wi 4   = wceq 1653  {csn 4367   “ cima 5314  [cec 7979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-rab 3097  df-v 3386  df-dif 3771  df-un 3773  df-in 3775  df-ss 3782  df-nul 4115  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4843  df-opab 4905  df-xp 5317  df-cnv 5319  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-ec 7983

This theorem is referenced by:  eceq1d  8020  ecelqsg  8039  snec  8047  qliftfun  8069  qliftfuns  8071  qliftval  8073  ecoptocl  8074  eroveu  8080  erov  8082  divsfval  16519  qusghm  18007  sylow1lem3  18325  efgi2  18448  frgpup3lem  18502  znzrhval  20213  qustgpopn  22248  qustgplem  22249  elpi1i  23170  pi1xfrf  23177  pi1xfrval  23178  pi1xfrcnvlem  23180  pi1cof  23183  pi1coval  23184  vitalilem3  23715  eceq1i  34529  prtlem9  34878  prtlem11  34880