Theorem abrexex 7939

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  {cab 2739  ∃wrex 3085  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-rep 5226

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3086  df-v 3455

This theorem is referenced by:  ab2rexex  7956  kmlem10  10113  cshwsexa  14834  shftfval  15080  dvdsrval  20389  cmpsublem  23439  cmpsub  23440  ptrescn  23679  addsproplem2  28040  negsid  28111  onaddscl  28347  recut  28564  elreno2  28565  satfvsuclem1  35673  fmlasuc0  35698  nmulprop  36504  heibor1lem  38272  pointsetN  40329  eldiophb  43302