Theorem fixssdm

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

	Ref	Expression
Assertion	fixssdm	$$⊢\mathrm{𝖥𝗂𝗑}A\subseteq \mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		df-fix	$$⊢\mathrm{𝖥𝗂𝗑}A=\mathrm{dom}\left(A\cap \mathrm{I}\right)$$
2		inss1	$$⊢A\cap \mathrm{I}\subseteq A$$
3		dmss	$$⊢A\cap \mathrm{I}\subseteq A\to \mathrm{dom}\left(A\cap \mathrm{I}\right)\subseteq \mathrm{dom}A$$
4	2 3	ax-mp	$$⊢\mathrm{dom}\left(A\cap \mathrm{I}\right)\subseteq \mathrm{dom}A$$
5	1 4	eqsstri	$$⊢\mathrm{𝖥𝗂𝗑}A\subseteq \mathrm{dom}A$$