Theorem dffix2

Description: The fixpoints of a class in terms of its range. (Contributed by Scott Fenton, 16-Apr-2012)

	Ref	Expression
Assertion	dffix2	|- Fix A = ran ( A i^i _I )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	elfix	|- ( x e. Fix A <-> x A x )
3	1	elrn	|- ( x e. ran ( A i^i _I ) <-> E. y y ( A i^i _I ) x )
4		brin	|- ( y ( A i^i _I ) x <-> ( y A x /\ y _I x ) )
5		ancom	|- ( ( y A x /\ y _I x ) <-> ( y _I x /\ y A x ) )
6	1	ideq	|- ( y _I x <-> y = x )
7	6	anbi1i	|- ( ( y _I x /\ y A x ) <-> ( y = x /\ y A x ) )
8	4 5 7	3bitri	|- ( y ( A i^i _I ) x <-> ( y = x /\ y A x ) )
9	8	exbii	|- ( E. y y ( A i^i _I ) x <-> E. y ( y = x /\ y A x ) )
10		breq1	|- ( y = x -> ( y A x <-> x A x ) )
11	10	equsexvw	|- ( E. y ( y = x /\ y A x ) <-> x A x )
12	3 9 11	3bitri	|- ( x e. ran ( A i^i _I ) <-> x A x )
13	2 12	bitr4i	|- ( x e. Fix A <-> x e. ran ( A i^i _I ) )
14	13	eqriv	|- Fix A = ran ( A i^i _I )