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	$$⊢\exists !yAFy\to \left(F\left(A\right)=y\leftrightarrow AFy\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfeu1	$$⊢Ⅎy\exists !yAFy$$
2		nfv	$$⊢ℲyAFF\left(A\right)$$
3		euex	$$⊢\exists !yAFy\to \exists yAFy$$
4		tz6.12-1	$$⊢\left(AFy\wedge \exists !yAFy\right)\to F\left(A\right)=y$$
5	4	expcom	$$⊢\exists !yAFy\to \left(AFy\to F\left(A\right)=y\right)$$
6		breq2	$$⊢F\left(A\right)=y\to \left(AFF\left(A\right)\leftrightarrow AFy\right)$$
7	6	biimprd	$$⊢F\left(A\right)=y\to \left(AFy\to AFF\left(A\right)\right)$$
8	5 7	syli	$$⊢\exists !yAFy\to \left(AFy\to AFF\left(A\right)\right)$$
9	1 2 3 8	exlimimdd	$$⊢\exists !yAFy\to AFF\left(A\right)$$
10	9 6	syl5ibcom	$$⊢\exists !yAFy\to \left(F\left(A\right)=y\to AFy\right)$$
11	10 5	impbid	$$⊢\exists !yAFy\to \left(F\left(A\right)=y\leftrightarrow AFy\right)$$