Theorem elfix

Description: Membership in the fixpoints of a class. (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Hypothesis	elfix.1	$$⊢A\in \mathrm{V}$$
Assertion	elfix	$$⊢A\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow ARA$$

Proof

Step	Hyp	Ref	Expression
1		elfix.1	$$⊢A\in \mathrm{V}$$
2		df-fix	$$⊢\mathrm{𝖥𝗂𝗑}R=\mathrm{dom}\left(R\cap \mathrm{I}\right)$$
3	2	eleq2i	$$⊢A\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow A\in \mathrm{dom}\left(R\cap \mathrm{I}\right)$$
4	1	eldm	$$⊢A\in \mathrm{dom}\left(R\cap \mathrm{I}\right)\leftrightarrow \exists xA\left(R\cap \mathrm{I}\right)x$$
5		brin	$$⊢A\left(R\cap \mathrm{I}\right)x\leftrightarrow \left(ARx\wedge A\mathrm{I}x\right)$$
6		ancom	$$⊢\left(ARx\wedge A\mathrm{I}x\right)\leftrightarrow \left(A\mathrm{I}x\wedge ARx\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	ideq	$$⊢A\mathrm{I}x\leftrightarrow A=x$$
9		eqcom	$$⊢A=x\leftrightarrow x=A$$
10	8 9	bitri	$$⊢A\mathrm{I}x\leftrightarrow x=A$$
11	10	anbi1i	$$⊢\left(A\mathrm{I}x\wedge ARx\right)\leftrightarrow \left(x=A\wedge ARx\right)$$
12	5 6 11	3bitri	$$⊢A\left(R\cap \mathrm{I}\right)x\leftrightarrow \left(x=A\wedge ARx\right)$$
13	12	exbii	$$⊢\exists xA\left(R\cap \mathrm{I}\right)x\leftrightarrow \exists x\left(x=A\wedge ARx\right)$$
14	4 13	bitri	$$⊢A\in \mathrm{dom}\left(R\cap \mathrm{I}\right)\leftrightarrow \exists x\left(x=A\wedge ARx\right)$$
15		breq2	$$⊢x=A\to \left(ARx\leftrightarrow ARA\right)$$
16	1 15	ceqsexv	$$⊢\exists x\left(x=A\wedge ARx\right)\leftrightarrow ARA$$
17	3 14 16	3bitri	$$⊢A\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow ARA$$