Theorem abrexex 7963

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2739  ∃wrex 3087  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-rep 5232

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3453

This theorem is used by:  ab2rexex  7980  kmlem10  10219  cshwsexa  14955  shftfval  15203  dvdsrval  20571  cmpsublem  23697  cmpsub  23698  ptrescn  23938  addsproplem2  28338  negsid  28409  onaddscl  28645  recut  28862  elreno2  28863  satfvsuclem1  36093  fmlasuc0  36118  nmulprop  36909  heibor1lem  38711  pointsetN  40766  eldiophb  43721