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

Theorem abrexex 7931
Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7929. See also abrexex2 7938. (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 7929 . 2 (𝐴 ∈ V → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
31, 2ax-mp 5 1 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106  {cab 2708  wrex 3069  Vcvv 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-rep 5278
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-mo 2533  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3475
This theorem is referenced by:  ab2rexex  7948  kmlem10  10136  cshwsexa  14756  shftfval  14999  dvdsrval  20127  cmpsublem  22832  cmpsub  22833  ptrescn  23072  addsproplem2  27370  negsid  27431  satfvsuclem1  34179  fmlasuc0  34204  heibor1lem  36480  pointsetN  38415  eldiophb  41264
  Copyright terms: Public domain W3C validator