Theorem rabex2 5335

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

Step	Hyp	Ref	Expression
1		rabex2.2	. 2 ⊢ 𝐴 ∈ V
2		rabex2.1	. . 3 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
3		id 22	. . 3 ⊢ (𝐴 ∈ V → 𝐴 ∈ V)
4	2, 3	rabexd 5334	. 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V)
5	1, 4	ax-mp 5	1 ⊢ 𝐵 ∈ V

Syntax hints:   = wceq 1542   ∈ wcel 2107  {crab 3433  Vcvv 3475

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 5300

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 3434  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  rab2ex  5336  mapfien2  9404  cantnffval  9658  nqex  10918  gsumvalx  18595  psgnfval  19368  odval  19402  sylow1lem2  19467  sylow3lem6  19500  ablfaclem1  19955  psrass1lemOLD  21493  psrass1lem  21496  psrbas  21497  psrelbas  21498  psrmulfval  21504  psrmulcllem  21506  psrvscaval  21511  psr0cl  21513  psr0lid  21514  psrnegcl  21515  psrlinv  21516  psr1cl  21522  psrlidm  21523  psrdi  21526  psrdir  21527  psrass23l  21528  psrcom  21529  psrass23  21530  mvrval  21541  mplsubglem  21558  mpllsslem  21559  mplsubrglem  21563  mplvscaval  21575  mplmon  21590  mplmonmul  21591  mplcoe1  21592  ltbval  21598  mplmon2  21622  evlslem2  21642  evlslem3  21643  evlslem1  21645  rrxmet  24925  mdegldg  25584  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvglem  26544  upgrres1lem1  28566  frgrwopreg1  29571  dlwwlknondlwlknonen  29619  nsgmgc  32523  nsgqusf1o  32527  eulerpartlem1  33366  eulerpartlemt  33370  eulerpartgbij  33371  ballotlemoex  33484  satffunlem2lem2  34397  mapdunirnN  40521  mplmapghm  41128  evlsvvvallem2  41134  selvvvval  41157  evlsmhpvvval  41167  pwfi2en  41839  smfresal  45504  oddiadd  46584  2zrngadd  46835  2zrngmul  46843