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