Theorem abrexex 7900

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2711  ∃wrex 3057  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-rep 5219

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3058  df-v 3439

This theorem is referenced by:  ab2rexex  7917  kmlem10  10058  cshwsexa  14733  shftfval  14979  dvdsrval  20281  cmpsublem  23315  cmpsub  23316  ptrescn  23555  addsproplem2  27914  negsid  27984  onaddscl  28211  recut  28399  0reno  28400  satfvsuclem1  35424  fmlasuc0  35449  heibor1lem  37869  pointsetN  39860  eldiophb  42874