Theorem eceq1 8713

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

Syntax hints:   → wi 4   = wceq 1540  {csn 4592   “ cima 5644  [cec 8672

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-ec 8676

This theorem is referenced by:  eceq1d  8714  ecelqs  8744  snec  8754  qliftfun  8778  qliftfuns  8780  qliftval  8782  ecoptocl  8783  eroveu  8788  erov  8790  divsfval  17517  qusghm  19194  sylow1lem3  19537  efgi2  19662  frgpup3lem  19714  rngqiprngimfv  21215  rngqiprngimf1  21217  rngqiprngimfo  21218  pzriprnglem11  21408  znzrhval  21463  qustgpopn  24014  qustgplem  24015  elpi1i  24953  pi1xfrf  24960  pi1xfrval  24961  pi1xfrcnvlem  24963  pi1cof  24966  pi1coval  24967  vitalilem3  25518  tgjustr  28408  qusker  33327  qusvscpbl  33329  qusvsval  33330  algextdeg  33722  eceq1i  38273  disjressuc2  38381  disjlem14  38797  prtlem9  38864  prtlem11  38866  aks6d1c6lem5  42172  aks5lem3a  42184