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	⊢ Ⅎ 𝑥 𝐶
Assertion	abrexss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		abrexss.1	⊢ Ⅎ 𝑥 𝐶
2		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶
3	1	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐶
4		eleq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 ) )
5		vex	⊢ 𝑧 ∈ V
6	5	a1i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → 𝑧 ∈ V )
7		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
8	2 3 4 6 7	elabreximd	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) → 𝑧 ∈ 𝐶 )
9	8	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑧 ∈ 𝐶 ) )
10	9	ssrdv	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ⊆ 𝐶 )