Theorem elfix2

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

	Ref	Expression
Hypothesis	elfix2.1	⊢ Rel 𝑅
Assertion	elfix2	⊢ ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 𝑅 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elfix2.1	⊢ Rel 𝑅
2		elex	⊢ ( 𝐴 ∈ Fix 𝑅 → 𝐴 ∈ V )
3	1	brrelex1i	⊢ ( 𝐴 𝑅 𝐴 → 𝐴 ∈ V )
4		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Fix 𝑅 ↔ 𝐴 ∈ Fix 𝑅 ) )
5		breq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
6	5	anidms	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑥 ↔ 𝐴 𝑅 𝐴 ) )
7		vex	⊢ 𝑥 ∈ V
8	7	elfix	⊢ ( 𝑥 ∈ Fix 𝑅 ↔ 𝑥 𝑅 𝑥 )
9	4 6 8	vtoclbg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 𝑅 𝐴 ) )
10	2 3 9	pm5.21nii	⊢ ( 𝐴 ∈ Fix 𝑅 ↔ 𝐴 𝑅 𝐴 )