Theorem abrexex 7915

Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7914. See also abrexex2 7922. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Hypothesis

Ref	Expression
abrexex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
abrexex	⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem abrexex

Step	Hyp	Ref	Expression
1		abrexex.1	. 2 ⊢ 𝐴 ∈ V
2		abrexexg 7914	. 2 ⊢ (𝐴 ∈ V → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2714  ∃wrex 3061  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-rep 5212

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-v 3431

This theorem is referenced by:  ab2rexex  7932  kmlem10  10082  cshwsexa  14786  shftfval  15032  dvdsrval  20341  cmpsublem  23364  cmpsub  23365  ptrescn  23604  addsproplem2  27962  negsid  28033  onaddscl  28269  recut  28486  elreno2  28487  satfvsuclem1  35541  fmlasuc0  35566  heibor1lem  38130  pointsetN  40187  eldiophb  43189