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 𝐴 = dom ( 𝐴 ∩ I )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cfix	⊢ Fix 𝐴
2		cid	⊢ I
3	0 2	cin	⊢ ( 𝐴 ∩ I )
4	3	cdm	⊢ dom ( 𝐴 ∩ I )
5	1 4	wceq	⊢ Fix 𝐴 = dom ( 𝐴 ∩ I )