This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )