Definition df-fix 30625

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

Assertion

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

Detailed syntax breakdown of Definition df-fix

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cfix 30601	. 2 class Fix A
3		cid 4744	. . . 4 class _I
4	1, 3	cin 3403	. . 3 class ( A i^i _I )
5	4	cdm 4834	. 2 class dom ( A i^i _I )
6	2, 5	wceq 1444	1 wff Fix A = dom ( A i^i _I )

This definition is referenced by:  elfix  30670  fixssdm  30673  fixun  30676