Theorem abrexss

Description: A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017)

	Ref	Expression
Hypothesis	abrexss.1	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	abrexss	$$⊢\forall x\in AB\in C\to \left\{y|\exists x\in Ay=B\right\}\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		abrexss.1	$$⊢\underset{\_}{Ⅎ}xC$$
2		nfra1	$$⊢Ⅎx\forall x\in AB\in C$$
3	1	nfcri	$$⊢Ⅎxz\in C$$
4		eleq1	$$⊢z=B\to \left(z\in C\leftrightarrow B\in C\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6	5	a1i	$$⊢\forall x\in AB\in C\to z\in \mathrm{V}$$
7		rspa	$$⊢\left(\forall x\in AB\in C\wedge x\in A\right)\to B\in C$$
8	2 3 4 6 7	elabreximd	$$⊢\left(\forall x\in AB\in C\wedge z\in \left\{y|\exists x\in Ay=B\right\}\right)\to z\in C$$
9	8	ex	$$⊢\forall x\in AB\in C\to \left(z\in \left\{y|\exists x\in Ay=B\right\}\to z\in C\right)$$
10	9	ssrdv	$$⊢\forall x\in AB\in C\to \left\{y|\exists x\in Ay=B\right\}\subseteq C$$