Theorem eceq1 8343

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 5906	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ {𝐴}) = (𝐶 “ {𝐵}))
3		df-ec 8307	. 2 ⊢ [𝐴]𝐶 = (𝐶 “ {𝐴})
4		df-ec 8307	. 2 ⊢ [𝐵]𝐶 = (𝐶 “ {𝐵})
5	2, 3, 4	3eqtr4g 2818	1 ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶)

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

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-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-opab 5099  df-xp 5534  df-cnv 5536  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-ec 8307

This theorem is referenced by:  eceq1d  8344  ecelqsg  8368  snec  8376  qliftfun  8398  qliftfuns  8400  qliftval  8402  ecoptocl  8403  eroveu  8408  erov  8410  divsfval  16891  qusghm  18475  sylow1lem3  18805  efgi2  18931  frgpup3lem  18983  znzrhval  20327  qustgpopn  22833  qustgplem  22834  elpi1i  23760  pi1xfrf  23767  pi1xfrval  23768  pi1xfrcnvlem  23770  pi1cof  23773  pi1coval  23774  vitalilem3  24323  tgjustr  26380  qusker  31082  qusvscpbl  31084  qusscaval  31085  eceq1i  36007  prtlem9  36474  prtlem11  36476