Theorem abrexex 7968

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {cab 2744  ∃wrex 3092  Vcvv 3458

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 2148  ax-9 2156  ax-ext 2738  ax-rep 5243

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-mo 2570  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-v 3460

This theorem is used by:  ab2rexex  7985  kmlem10  10162  cshwsexa  14887  shftfval  15133  dvdsrval  20476  cmpsublem  23593  cmpsub  23594  ptrescn  23833  addsproplem2  28200  negsid  28271  onaddscl  28507  recut  28724  elreno2  28725  satfvsuclem1  35872  fmlasuc0  35897  nmulprop  36703  heibor1lem  38501  pointsetN  40556  eldiophb  43529