This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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