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

Theorem rabex2 4966
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 4965 . 2 (𝐴 ∈ V → 𝐵 ∈ V)
51, 4ax-mp 5 1 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2139  {crab 3054  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-in 3722  df-ss 3729
This theorem is referenced by:  rab2ex  4967  mapfien2  8479  cantnffval  8733  nqex  9937  gsumvalx  17471  psgnfval  18120  odval  18153  sylow1lem2  18214  sylow3lem6  18247  ablfaclem1  18684  psrass1lem  19579  psrbas  19580  psrelbas  19581  psrmulfval  19587  psrmulcllem  19589  psrvscaval  19594  psr0cl  19596  psr0lid  19597  psrnegcl  19598  psrlinv  19599  psr1cl  19604  psrlidm  19605  psrdi  19608  psrdir  19609  psrass23l  19610  psrcom  19611  psrass23  19612  mvrval  19623  mplsubglem  19636  mpllsslem  19637  mplsubrglem  19641  mplvscaval  19650  mplmon  19665  mplmonmul  19666  mplcoe1  19667  ltbval  19673  opsrtoslem2  19687  mplmon2  19695  evlslem2  19714  evlslem3  19716  evlslem1  19717  rrxmet  23391  mdegldg  24025  lgamgulmlem5  24958  lgamgulmlem6  24959  lgamgulm2  24961  lgamcvglem  24965  upgrres1lem1  26400  frgrwopreg1  27472  dlwwlknondlwlknonen  27527  eulerpartlem1  30738  eulerpartlemt  30742  eulerpartgbij  30743  ballotlemoex  30856  mapdunirnN  37441  pwfi2en  38169  smfresal  41501  oddiadd  42324  2zrngadd  42447  2zrngmul  42455
  Copyright terms: Public domain W3C validator