dffix2

Description: The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012)

		Ref	Expression
	Assertion	dffix2	$⊢ 𝖥𝗂𝗑 A = ran (A \cap I)$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	elfix	$⊢ x \in 𝖥𝗂𝗑 A \leftrightarrow x A x$
3	1	elrn	$⊢ x \in ran (A \cap I) \leftrightarrow \exists y y (A \cap I) x$
4		brin	$⊢ y (A \cap I) x \leftrightarrow (y A x \land y I x)$
5		ancom	$⊢ (y A x \land y I x) \leftrightarrow (y I x \land y A x)$
6	1	ideq	$⊢ y I x \leftrightarrow y = x$
7	6	anbi1i	$⊢ (y I x \land y A x) \leftrightarrow (y = x \land y A x)$
8	4 5 7	3bitri	$⊢ y (A \cap I) x \leftrightarrow (y = x \land y A x)$
9	8	exbii	$⊢ \exists y y (A \cap I) x \leftrightarrow \exists y (y = x \land y A x)$
10		breq1	$⊢ y = x \to (y A x \leftrightarrow x A x)$
11	10	equsexvw	$⊢ \exists y (y = x \land y A x) \leftrightarrow x A x$
12	3 9 11	3bitri	$⊢ x \in ran (A \cap I) \leftrightarrow x A x$
13	2 12	bitr4i	$⊢ x \in 𝖥𝗂𝗑 A \leftrightarrow x \in ran (A \cap I)$
14	13	eqriv	$⊢ 𝖥𝗂𝗑 A = ran (A \cap I)$

Metamath Proof Explorer