Theorem tz6.12c

Description: Corollary of Theorem 6.12(1) of TakeutiZaring p. 27. (Contributed by NM, 30-Apr-2004)

	Ref	Expression
Assertion	tz6.12c	|- ( E! y A F y -> ( ( F ` A ) = y <-> A F y ) )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	|- F/ y E! y A F y
2		nfv	|- F/ y A F ( F ` A )
3		euex	|- ( E! y A F y -> E. y A F y )
4		tz6.12-1	|- ( ( A F y /\ E! y A F y ) -> ( F ` A ) = y )
5	4	expcom	|- ( E! y A F y -> ( A F y -> ( F ` A ) = y ) )
6		breq2	|- ( ( F ` A ) = y -> ( A F ( F ` A ) <-> A F y ) )
7	6	biimprd	|- ( ( F ` A ) = y -> ( A F y -> A F ( F ` A ) ) )
8	5 7	syli	|- ( E! y A F y -> ( A F y -> A F ( F ` A ) ) )
9	1 2 3 8	exlimimdd	|- ( E! y A F y -> A F ( F ` A ) )
10	9 6	syl5ibcom	|- ( E! y A F y -> ( ( F ` A ) = y -> A F y ) )
11	10 5	impbid	|- ( E! y A F y -> ( ( F ` A ) = y <-> A F y ) )