Definition df-fix 35854

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

Assertion

Ref	Expression
df-fix	⊢ Fix 𝐴 = dom (𝐴 ∩ I )

Detailed syntax breakdown of Definition df-fix

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cfix 35830	. 2 class Fix 𝐴
3		cid 5586	. . . 4 class I
4	1, 3	cin 3965	. . 3 class (𝐴 ∩ I )
5	4	cdm 5693	. 2 class dom (𝐴 ∩ I )
6	2, 5	wceq 1539	1 wff Fix 𝐴 = dom (𝐴 ∩ I )

This definition is referenced by:  elfix  35898  fixssdm  35901  fixun  35904