Theorem abrexex 7906

Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7905. See also abrexex2 7913. (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 7905	. 2 ⊢ (𝐴 ∈ V → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ∈ V

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2714  ∃wrex 3060  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-rep 5224

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-v 3442

This theorem is referenced by:  ab2rexex  7923  kmlem10  10070  cshwsexa  14747  shftfval  14993  dvdsrval  20297  cmpsublem  23343  cmpsub  23344  ptrescn  23583  addsproplem2  27966  negsid  28037  onaddscl  28273  recut  28490  elreno2  28491  satfvsuclem1  35553  fmlasuc0  35578  heibor1lem  38006  pointsetN  39997  eldiophb  42995