Theorem elfix2

Description: Alternative membership in the fixpoint of a class. (Contributed by Scott Fenton, 11-Apr-2012)

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

Proof

Step	Hyp	Ref	Expression
1		elfix2.1	$$⊢\mathrm{Rel}R$$
2		elex	$$⊢A\in \mathrm{𝖥𝗂𝗑}R\to A\in \mathrm{V}$$
3	1	brrelex1i	$$⊢ARA\to A\in \mathrm{V}$$
4		eleq1	$$⊢x=A\to \left(x\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow A\in \mathrm{𝖥𝗂𝗑}R\right)$$
5		breq12	$$⊢\left(x=A\wedge x=A\right)\to \left(xRx\leftrightarrow ARA\right)$$
6	5	anidms	$$⊢x=A\to \left(xRx\leftrightarrow ARA\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8	7	elfix	$$⊢x\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow xRx$$
9	4 6 8	vtoclbg	$$⊢A\in \mathrm{V}\to \left(A\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow ARA\right)$$
10	2 3 9	pm5.21nii	$$⊢A\in \mathrm{𝖥𝗂𝗑}R\leftrightarrow ARA$$