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	⊢ Fix 𝐴 ⊆ dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-fix	⊢ Fix 𝐴 = dom ( 𝐴 ∩ I )
2		inss1	⊢ ( 𝐴 ∩ I ) ⊆ 𝐴
3		dmss	⊢ ( ( 𝐴 ∩ I ) ⊆ 𝐴 → dom ( 𝐴 ∩ I ) ⊆ dom 𝐴 )
4	2 3	ax-mp	⊢ dom ( 𝐴 ∩ I ) ⊆ dom 𝐴
5	1 4	eqsstri	⊢ Fix 𝐴 ⊆ dom 𝐴