Theorem 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 e. Fix R <-> A R A )

Proof

Step	Hyp	Ref	Expression
1		elfix2.1	|- Rel R
2		elex	|- ( A e. Fix R -> A e. _V )
3	1	brrelex1i	|- ( A R A -> A e. _V )
4		eleq1	|- ( x = A -> ( x e. Fix R <-> A e. Fix R ) )
5		breq12	|- ( ( x = A /\ x = A ) -> ( x R x <-> A R A ) )
6	5	anidms	|- ( x = A -> ( x R x <-> A R A ) )
7		vex	|- x e. _V
8	7	elfix	|- ( x e. Fix R <-> x R x )
9	4 6 8	vtoclbg	|- ( A e. _V -> ( A e. Fix R <-> A R A ) )
10	2 3 9	pm5.21nii	|- ( A e. Fix R <-> A R A )