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  8481  cantnffval  8735  nqex  9957  gsumvalx  17491  psgnfval  18140  odval  18173  sylow1lem2  18234  sylow3lem6  18267  ablfaclem1  18704  psrass1lem  19599  psrbas  19600  psrelbas  19601  psrmulfval  19607  psrmulcllem  19609  psrvscaval  19614  psr0cl  19616  psr0lid  19617  psrnegcl  19618  psrlinv  19619  psr1cl  19624  psrlidm  19625  psrdi  19628  psrdir  19629  psrass23l  19630  psrcom  19631  psrass23  19632  mvrval  19643  mplsubglem  19656  mpllsslem  19657  mplsubrglem  19661  mplvscaval  19670  mplmon  19685  mplmonmul  19686  mplcoe1  19687  ltbval  19693  opsrtoslem2  19707  mplmon2  19715  evlslem2  19734  evlslem3  19736  evlslem1  19737  rrxmet  23411  mdegldg  24045  lgamgulmlem5  24979  lgamgulmlem6  24980  lgamgulm2  24982  lgamcvglem  24986  upgrres1lem1  26421  frgrwopreg1  27493  dlwwlknondlwlknonen  27548  eulerpartlem1  30759  eulerpartlemt  30763  eulerpartgbij  30764  ballotlemoex  30877  mapdunirnN  37459  pwfi2en  38187  smfresal  41519  oddiadd  42342  2zrngadd  42465  2zrngmul  42473
  Copyright terms: Public domain W3C validator