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	|- F/_ x C
Assertion	abrexss	|- ( A. x e. A B e. C -> { y | E. x e. A y = B } C_ C )

Proof

Step	Hyp	Ref	Expression
1		abrexss.1	|- F/_ x C
2		nfra1	|- F/ x A. x e. A B e. C
3	1	nfcri	|- F/ x z e. C
4		eleq1	|- ( z = B -> ( z e. C <-> B e. C ) )
5		vex	|- z e. _V
6	5	a1i	|- ( A. x e. A B e. C -> z e. _V )
7		rspa	|- ( ( A. x e. A B e. C /\ x e. A ) -> B e. C )
8	2 3 4 6 7	elabreximd	|- ( ( A. x e. A B e. C /\ z e. { y | E. x e. A y = B } ) -> z e. C )
9	8	ex	|- ( A. x e. A B e. C -> ( z e. { y | E. x e. A y = B } -> z e. C ) )
10	9	ssrdv	|- ( A. x e. A B e. C -> { y | E. x e. A y = B } C_ C )