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

Theorem rabex2 5295
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 5294 . 2 (𝐴 ∈ V → 𝐵 ∈ V)
51, 4ax-mp 5 1 𝐵 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {crab 3406  Vcvv 3447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5260
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-in 3921  df-ss 3931
This theorem is referenced by:  rab2ex  5296  mapfien2  9353  cantnffval  9607  nqex  10867  gsumvalx  18539  psgnfval  19290  odval  19324  sylow1lem2  19389  sylow3lem6  19422  ablfaclem1  19872  psrass1lemOLD  21365  psrass1lem  21368  psrbas  21369  psrelbas  21370  psrmulfval  21376  psrmulcllem  21378  psrvscaval  21383  psr0cl  21385  psr0lid  21386  psrnegcl  21387  psrlinv  21388  psr1cl  21394  psrlidm  21395  psrdi  21398  psrdir  21399  psrass23l  21400  psrcom  21401  psrass23  21402  mvrval  21413  mplsubglem  21428  mpllsslem  21429  mplsubrglem  21433  mplvscaval  21443  mplmon  21459  mplmonmul  21460  mplcoe1  21461  ltbval  21467  mplmon2  21492  evlslem2  21512  evlslem3  21513  evlslem1  21515  rrxmet  24795  mdegldg  25454  lgamgulmlem5  26405  lgamgulmlem6  26406  lgamgulm2  26408  lgamcvglem  26412  upgrres1lem1  28306  frgrwopreg1  29311  dlwwlknondlwlknonen  29359  nsgmgc  32245  nsgqusf1o  32249  eulerpartlem1  33031  eulerpartlemt  33035  eulerpartgbij  33036  ballotlemoex  33149  satffunlem2lem2  34064  mapdunirnN  40163  pwfi2en  41471  smfresal  45119  oddiadd  46198  2zrngadd  46325  2zrngmul  46333
  Copyright terms: Public domain W3C validator