Theorem dffix2

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

	Ref	Expression
Assertion	dffix2	$$⊢\mathrm{𝖥𝗂𝗑}A=\mathrm{ran}\left(A\cap \mathrm{I}\right)$$

Proof

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