Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 df-fix 
 |-  Fix A = dom ( A i^i _I )
2 inss1 
 |-  ( A i^i _I ) C_ A
3 dmss 
 |-  ( ( A i^i _I ) C_ A -> dom ( A i^i _I ) C_ dom A )
4 2 3 ax-mp 
 |-  dom ( A i^i _I ) C_ dom A
5 1 4 eqsstri 
 |-  Fix A C_ dom A