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 2740  ∃wrex 3088  Vcvv 3453

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 2734  ax-rep 5236

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3455

This theorem is used by:  ab2rexex  7980  kmlem10  10166  cshwsexa  14899  shftfval  15147  dvdsrval  20508  cmpsublem  23630  cmpsub  23631  ptrescn  23871  addsproplem2  28243  negsid  28314  onaddscl  28550  recut  28767  elreno2  28768  satfvsuclem1  35946  fmlasuc0  35971  nmulprop  36778  heibor1lem  38567  pointsetN  40622  eldiophb  43610