Theorem elfix

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

	Ref	Expression
Hypothesis	elfix.1	|- A e. _V
Assertion	elfix	|- ( A e. Fix R <-> A R A )

Proof

Step	Hyp	Ref	Expression
1		elfix.1	|- A e. _V
2		df-fix	|- Fix R = dom ( R i^i _I )
3	2	eleq2i	|- ( A e. Fix R <-> A e. dom ( R i^i _I ) )
4	1	eldm	|- ( A e. dom ( R i^i _I ) <-> E. x A ( R i^i _I ) x )
5		brin	|- ( A ( R i^i _I ) x <-> ( A R x /\ A _I x ) )
6		ancom	|- ( ( A R x /\ A _I x ) <-> ( A _I x /\ A R x ) )
7		vex	|- x e. _V
8	7	ideq	|- ( A _I x <-> A = x )
9		eqcom	|- ( A = x <-> x = A )
10	8 9	bitri	|- ( A _I x <-> x = A )
11	10	anbi1i	|- ( ( A _I x /\ A R x ) <-> ( x = A /\ A R x ) )
12	5 6 11	3bitri	|- ( A ( R i^i _I ) x <-> ( x = A /\ A R x ) )
13	12	exbii	|- ( E. x A ( R i^i _I ) x <-> E. x ( x = A /\ A R x ) )
14	4 13	bitri	|- ( A e. dom ( R i^i _I ) <-> E. x ( x = A /\ A R x ) )
15		breq2	|- ( x = A -> ( A R x <-> A R A ) )
16	1 15	ceqsexv	|- ( E. x ( x = A /\ A R x ) <-> A R A )
17	3 14 16	3bitri	|- ( A e. Fix R <-> A R A )