Definition df-fix 5741

Description: Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-fix	|- FixA = ran (A i^i _I )

Detailed syntax breakdown of Definition df-fix

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cfix 5740	. 2 class FixA
3		cid 4764	. . . 4 class _I
4	1, 3	cin 3209	. . 3 class (A i^i _I )
5	4	crn 4774	. 2 class ran (A i^i _I )
6	2, 5	wceq 1642	1 wff FixA = ran (A i^i _I )

This definition is referenced by:  elfix  5788  fixexg  5789