Theorem abrexex 7953

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  {cab 2708  ∃wrex 3069  Vcvv 3473

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-rep 5285

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-mo 2533  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3475

This theorem is referenced by:  ab2rexex  7970  kmlem10  10160  cshwsexa  14781  shftfval  15024  dvdsrval  20259  cmpsublem  23223  cmpsub  23224  ptrescn  23463  addsproplem2  27801  negsid  27867  recut  28105  0reno  28106  satfvsuclem1  34815  fmlasuc0  34840  heibor1lem  37143  pointsetN  39078  eldiophb  41960