Theorem tz6.12cOLD

Description: Obsolete version of tz6.12c as of 23-Dec-2024. (Contributed by NM, 30-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	tz6.12cOLD	|- ( 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 ) )