Metamath Proof Explorer


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 𝐴