Metamath Proof Explorer

Definition df-fix

Description: Define the class of all fixpoints of a relationship. (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Assertion df-fix 
|- Fix A = dom ( A i^i _I )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 0 cfix 
 |-  Fix A
2 cid 
 |-  _I
3 0 2 cin 
 |-  ( A i^i _I )
4 3 cdm 
 |-  dom ( A i^i _I )
5 1 4 wceq 
 |-  Fix A = dom ( A i^i _I )