Theorem abrexex 7947

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

Syntax hints:   = wceq 1563   ∈ wcel 2145  {cab 2743  ∃wrex 3089  Vcvv 3457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-rep 5232

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-mo 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3090  df-v 3459

This theorem is referenced by:  ab2rexex  7964  kmlem10  10131  cshwsexa  14851  shftfval  15097  dvdsrval  20434  cmpsublem  23517  cmpsub  23518  ptrescn  23757  addsproplem2  28121  negsid  28192  onaddscl  28428  recut  28645  elreno2  28646  satfvsuclem1  35722  fmlasuc0  35747  nmulprop  36553  heibor1lem  38320  pointsetN  40377  eldiophb  43350