Metamath Proof Explorer

Theorem ecss

Description: An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis ecss.1 
|- ( ph -> R Er X )
Assertion ecss 
|- ( ph -> [ A ] R C_ X )

Proof

Step Hyp Ref Expression
1 ecss.1 
 |-  ( ph -> R Er X )
2 df-ec 
 |-  [ A ] R = ( R " { A } )
3 imassrn 
 |-  ( R " { A } ) C_ ran R
4 2 3 eqsstri 
 |-  [ A ] R C_ ran R
5 errn 
 |-  ( R Er X -> ran R = X )
6 1 5 syl 
 |-  ( ph -> ran R = X )
7 4 6 sseqtrid 
 |-  ( ph -> [ A ] R C_ X )