Theorem abrexex 7960

Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7959. See also abrexex2 7967. (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 1570   ∈ wcel 2143  {cab 2741  ∃wrex 3089  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-rep 5239

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3457

This theorem is referenced by:  ab2rexex  7977  kmlem10  10144  cshwsexa  14863  shftfval  15109  dvdsrval  20444  cmpsublem  23537  cmpsub  23538  ptrescn  23777  addsproplem2  28141  negsid  28212  onaddscl  28448  recut  28665  elreno2  28666  satfvsuclem1  35829  fmlasuc0  35854  nmulprop  36660  heibor1lem  38438  pointsetN  40493  eldiophb  43468