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

Theorem rabex2 5233
Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by AV, 16-Jul-2019.) (Revised by AV, 26-Mar-2021.)
Hypotheses
Ref Expression
rabex2.1 𝐵 = {𝑥𝐴𝜓}
rabex2.2 𝐴 ∈ V
Assertion
Ref Expression
rabex2 𝐵 ∈ V
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝜓(𝑥)   𝐵(𝑥)

Proof of Theorem rabex2
StepHypRef Expression
1 rabex2.2 . 2 𝐴 ∈ V
2 rabex2.1 . . 3 𝐵 = {𝑥𝐴𝜓}
3 id 22 . . 3 (𝐴 ∈ V → 𝐴 ∈ V)
42, 3rabexd 5232 . 2 (𝐴 ∈ V → 𝐵 ∈ V)
51, 4ax-mp 5 1 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2106  {crab 3146  Vcvv 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-in 3946  df-ss 3955
This theorem is referenced by:  rab2ex  5234  mapfien2  8864  cantnffval  9118  nqex  10337  gsumvalx  17877  psgnfval  18550  odval  18584  sylow1lem2  18646  sylow3lem6  18679  ablfaclem1  19129  psrass1lem  20078  psrbas  20079  psrelbas  20080  psrmulfval  20086  psrmulcllem  20088  psrvscaval  20093  psr0cl  20095  psr0lid  20096  psrnegcl  20097  psrlinv  20098  psr1cl  20103  psrlidm  20104  psrdi  20107  psrdir  20108  psrass23l  20109  psrcom  20110  psrass23  20111  mvrval  20122  mplsubglem  20135  mpllsslem  20136  mplsubrglem  20140  mplvscaval  20149  mplmon  20164  mplmonmul  20165  mplcoe1  20166  ltbval  20172  opsrtoslem2  20185  mplmon2  20193  evlslem2  20212  evlslem3  20213  evlslem1  20215  rrxmet  23926  mdegldg  24575  lgamgulmlem5  25524  lgamgulmlem6  25525  lgamgulm2  25527  lgamcvglem  25531  upgrres1lem1  27006  frgrwopreg1  28012  dlwwlknondlwlknonen  28060  eulerpartlem1  31512  eulerpartlemt  31516  eulerpartgbij  31517  ballotlemoex  31630  satffunlem2lem2  32538  mapdunirnN  38654  pwfi2en  39559  smfresal  42926  oddiadd  43910  2zrngadd  44037  2zrngmul  44045
  Copyright terms: Public domain W3C validator