This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
Assertion ecss ( 𝜑 → [ 𝐴 ] 𝑅 ⊆ 𝑋 )

Proof

Step Hyp Ref Expression
1 ecss.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2 df-ec ⊢ [ 𝐴 ] 𝑅 = ( 𝑅 “ { 𝐴 } )
3 imassrn ⊢ ( 𝑅 “ { 𝐴 } ) ⊆ ran 𝑅
4 2 3 eqsstri ⊢ [ 𝐴 ] 𝑅 ⊆ ran 𝑅
5 errn ⊢ ( 𝑅 Er 𝑋 → ran 𝑅 = 𝑋 )
6 1 5 syl ⊢ ( 𝜑 → ran 𝑅 = 𝑋 )
7 4 6 sseqtrid ⊢ ( 𝜑 → [ 𝐴 ] 𝑅 ⊆ 𝑋 )