Theorem tz6.12i

Description: Corollary of Theorem 6.12(2) of TakeutiZaring p. 27. (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	tz6.12i	$$⊢B\ne \varnothing \to \left(F\left(A\right)=B\to AFB\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
2		neeq1	$$⊢F\left(A\right)=y\to \left(F\left(A\right)\ne \varnothing \leftrightarrow y\ne \varnothing \right)$$
3		tz6.12-2	$$⊢\neg \exists !yAFy\to F\left(A\right)=\varnothing$$
4	3	necon1ai	$$⊢F\left(A\right)\ne \varnothing \to \exists !yAFy$$
5		tz6.12c	$$⊢\exists !yAFy\to \left(F\left(A\right)=y\leftrightarrow AFy\right)$$
6	4 5	syl	$$⊢F\left(A\right)\ne \varnothing \to \left(F\left(A\right)=y\leftrightarrow AFy\right)$$
7	6	biimpcd	$$⊢F\left(A\right)=y\to \left(F\left(A\right)\ne \varnothing \to AFy\right)$$
8	2 7	sylbird	$$⊢F\left(A\right)=y\to \left(y\ne \varnothing \to AFy\right)$$
9	8	eqcoms	$$⊢y=F\left(A\right)\to \left(y\ne \varnothing \to AFy\right)$$
10		neeq1	$$⊢y=F\left(A\right)\to \left(y\ne \varnothing \leftrightarrow F\left(A\right)\ne \varnothing \right)$$
11		breq2	$$⊢y=F\left(A\right)\to \left(AFy\leftrightarrow AFF\left(A\right)\right)$$
12	9 10 11	3imtr3d	$$⊢y=F\left(A\right)\to \left(F\left(A\right)\ne \varnothing \to AFF\left(A\right)\right)$$
13	1 12	vtocle	$$⊢F\left(A\right)\ne \varnothing \to AFF\left(A\right)$$
14	13	a1i	$$⊢F\left(A\right)=B\to \left(F\left(A\right)\ne \varnothing \to AFF\left(A\right)\right)$$
15		neeq1	$$⊢F\left(A\right)=B\to \left(F\left(A\right)\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
16		breq2	$$⊢F\left(A\right)=B\to \left(AFF\left(A\right)\leftrightarrow AFB\right)$$
17	14 15 16	3imtr3d	$$⊢F\left(A\right)=B\to \left(B\ne \varnothing \to AFB\right)$$
18	17	com12	$$⊢B\ne \varnothing \to \left(F\left(A\right)=B\to AFB\right)$$