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	$$⊢\mathrm{𝖥𝗂𝗑}A=\mathrm{dom}\left(A\cap \mathrm{I}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cfix	$$class\mathrm{𝖥𝗂𝗑}A$$
2		cid	$$class\mathrm{I}$$
3	0 2	cin	$$class\left(A\cap \mathrm{I}\right)$$
4	3	cdm	$$class\mathrm{dom}\left(A\cap \mathrm{I}\right)$$
5	1 4	wceq	$$wff\mathrm{𝖥𝗂𝗑}A=\mathrm{dom}\left(A\cap \mathrm{I}\right)$$