elfix2

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

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

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

Metamath Proof Explorer