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

Theorem abrexex 7986
Description: Existence of a class abstraction of existentially restricted sets. See the comment of abrexexg 7984. See also abrexex2 7993. (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 7984 . 2 (𝐴 ∈ V → {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V)
31, 2ax-mp 5 1 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  {cab 2712  wrex 3068  Vcvv 3478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-rep 5285
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-mo 2538  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-v 3480
This theorem is referenced by:  ab2rexex  8003  kmlem10  10198  cshwsexa  14859  shftfval  15106  dvdsrval  20378  cmpsublem  23423  cmpsub  23424  ptrescn  23663  addsproplem2  28018  negsid  28088  onaddscl  28301  recut  28443  0reno  28444  satfvsuclem1  35344  fmlasuc0  35369  heibor1lem  37796  pointsetN  39724  eldiophb  42745
  Copyright terms: Public domain W3C validator