Theorem abrexex 7961

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {cab 2713  ∃wrex 3060  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-rep 5249

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461

This theorem is referenced by:  ab2rexex  7978  kmlem10  10174  cshwsexa  14842  shftfval  15089  dvdsrval  20321  cmpsublem  23337  cmpsub  23338  ptrescn  23577  addsproplem2  27929  negsid  27999  onaddscl  28226  recut  28399  0reno  28400  satfvsuclem1  35381  fmlasuc0  35406  heibor1lem  37833  pointsetN  39760  eldiophb  42780