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	$$⊢\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)$$