MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abrexex Structured version   Visualization version   GIF version

Theorem abrexex 7987
Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7985. See also abrexex2 7994. (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
StepHypRef Expression
1 abrexex.1 . 2 𝐴 ∈ V
2 abrexexg 7985 . 2 (𝐴 ∈ V → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
31, 2ax-mp 5 1 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  {cab 2714  wrex 3070  Vcvv 3480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-rep 5279
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482
This theorem is referenced by:  ab2rexex  8004  kmlem10  10200  cshwsexa  14862  shftfval  15109  dvdsrval  20361  cmpsublem  23407  cmpsub  23408  ptrescn  23647  addsproplem2  28003  negsid  28073  onaddscl  28286  recut  28428  0reno  28429  satfvsuclem1  35364  fmlasuc0  35389  heibor1lem  37816  pointsetN  39743  eldiophb  42768
  Copyright terms: Public domain W3C validator