# Metamath Proof Explorer

## 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{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
Assertion abrexss ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in {C}\to \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}={B}\right\}\subseteq {C}$

### Proof

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