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	$$⊢\mathrm{𝖥𝗂𝗑}A\subseteq \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		dffix2	$$⊢\mathrm{𝖥𝗂𝗑}A=\mathrm{ran}\left(A\cap \mathrm{I}\right)$$
2		inss1	$$⊢A\cap \mathrm{I}\subseteq A$$
3	2	rnssi	$$⊢\mathrm{ran}\left(A\cap \mathrm{I}\right)\subseteq \mathrm{ran}A$$
4	1 3	eqsstri	$$⊢\mathrm{𝖥𝗂𝗑}A\subseteq \mathrm{ran}A$$