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 A C_ ran A

Proof

Step Hyp Ref Expression
1 dffix2 
 |-  Fix A = ran ( A i^i _I )
2 inss1 
 |-  ( A i^i _I ) C_ A
3 2 rnssi 
 |-  ran ( A i^i _I ) C_ ran A
4 1 3 eqsstri 
 |-  Fix A C_ ran A