Theorem tz6.12c-afv2

Description: Corollary of Theorem 6.12(1) of TakeutiZaring p. 27, analogous to tz6.12c . (Contributed by AV, 5-Sep-2022)

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