Theorem eceq1 8710

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

Syntax hints:   → wi 4   = wceq 1540  {csn 4589   “ cima 5641  [cec 8669

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ec 8673

This theorem is referenced by:  eceq1d  8711  ecelqs  8741  snec  8751  qliftfun  8775  qliftfuns  8777  qliftval  8779  ecoptocl  8780  eroveu  8785  erov  8787  divsfval  17510  qusghm  19187  sylow1lem3  19530  efgi2  19655  frgpup3lem  19707  rngqiprngimfv  21208  rngqiprngimf1  21210  rngqiprngimfo  21211  pzriprnglem11  21401  znzrhval  21456  qustgpopn  24007  qustgplem  24008  elpi1i  24946  pi1xfrf  24953  pi1xfrval  24954  pi1xfrcnvlem  24956  pi1cof  24959  pi1coval  24960  vitalilem3  25511  tgjustr  28401  qusker  33320  qusvscpbl  33322  qusvsval  33323  algextdeg  33715  eceq1i  38266  disjressuc2  38374  disjlem14  38790  prtlem9  38857  prtlem11  38859  aks6d1c6lem5  42165  aks5lem3a  42177