Theorem abrexex 7974

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {cab 2738  ∃wrex 3086  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-rep 5231

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452

This theorem is used by:  ab2rexex  7991  kmlem10  10241  cshwsexa  14979  shftfval  15228  dvdsrval  20596  cmpsublem  23722  cmpsub  23723  ptrescn  23963  addsproplem2  28361  negsid  28432  onaddscl  28668  recut  28885  elreno2  28886  satfvsuclem1  36210  fmlasuc0  36235  nmulprop  37031  heibor1lem  38836  pointsetN  40891  eldiophb  43861