Definition df-fix 5740

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

Assertion

Ref	Expression
df-fix	⊢ Fix A = ran (A ∩ I )

Detailed syntax breakdown of Definition df-fix

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cfix 5739	. 2 class Fix A
3		cid 4763	. . . 4 class I
4	1, 3	cin 3208	. . 3 class (A ∩ I )
5	4	crn 4773	. 2 class ran (A ∩ I )
6	2, 5	wceq 1642	1 wff Fix A = ran (A ∩ I )

This definition is referenced by:  elfix  5787  fixexg  5788