Theorem funimassd

Description: Sufficient condition for the image of a function being a subclass. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	funimassd.1	$$⊢Ⅎx\phi$$
	funimassd.2	$$⊢\phi \to \mathrm{Fun}F$$
	funimassd.3	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
Assertion	funimassd	$$⊢\phi \to F\left[A\right]\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		funimassd.1	$$⊢Ⅎx\phi$$
2		funimassd.2	$$⊢\phi \to \mathrm{Fun}F$$
3		funimassd.3	$$⊢\left(\phi \wedge x\in A\right)\to F\left(x\right)\in B$$
4		fvelima	$$⊢\left(\mathrm{Fun}F\wedge y\in F\left[A\right]\right)\to \exists x\in AF\left(x\right)=y$$
5	2 4	sylan	$$⊢\left(\phi \wedge y\in F\left[A\right]\right)\to \exists x\in AF\left(x\right)=y$$
6		nfv	$$⊢Ⅎxy\in F\left[A\right]$$
7	1 6	nfan	$$⊢Ⅎx\left(\phi \wedge y\in F\left[A\right]\right)$$
8		nfv	$$⊢Ⅎxy\in B$$
9		id	$$⊢F\left(x\right)=y\to F\left(x\right)=y$$
10	9	eqcomd	$$⊢F\left(x\right)=y\to y=F\left(x\right)$$
11	10	3ad2ant3	$$⊢\left(\phi \wedge x\in A\wedge F\left(x\right)=y\right)\to y=F\left(x\right)$$
12	3	3adant3	$$⊢\left(\phi \wedge x\in A\wedge F\left(x\right)=y\right)\to F\left(x\right)\in B$$
13	11 12	eqeltrd	$$⊢\left(\phi \wedge x\in A\wedge F\left(x\right)=y\right)\to y\in B$$
14	13	3exp	$$⊢\phi \to \left(x\in A\to \left(F\left(x\right)=y\to y\in B\right)\right)$$
15	14	adantr	$$⊢\left(\phi \wedge y\in F\left[A\right]\right)\to \left(x\in A\to \left(F\left(x\right)=y\to y\in B\right)\right)$$
16	7 8 15	rexlimd	$$⊢\left(\phi \wedge y\in F\left[A\right]\right)\to \left(\exists x\in AF\left(x\right)=y\to y\in B\right)$$
17	5 16	mpd	$$⊢\left(\phi \wedge y\in F\left[A\right]\right)\to y\in B$$
18	17	ssd	$$⊢\phi \to F\left[A\right]\subseteq B$$