Theorem fixssrn

Description: The fixpoints of a class are a subset of its range. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	fixssrn	⊢ Fix 𝐴 ⊆ ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		dffix2	⊢ Fix 𝐴 = ran ( 𝐴 ∩ I )
2		inss1	⊢ ( 𝐴 ∩ I ) ⊆ 𝐴
3	2	rnssi	⊢ ran ( 𝐴 ∩ I ) ⊆ ran 𝐴
4	1 3	eqsstri	⊢ Fix 𝐴 ⊆ ran 𝐴