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  28597  frgrwopreg1  29602  dlwwlknondlwlknonen  29650  nsgmgc  32554  nsgqusf1o  32558  eulerpartlem1  33397  eulerpartlemt  33401  eulerpartgbij  33402  ballotlemoex  33515  satffunlem2lem2  34428  mapdunirnN  40569  mplmapghm  41176  evlsvvvallem2  41182  selvvvval  41205  evlsmhpvvval  41215  pwfi2en  41887  smfresal  45552  oddiadd  46632  2zrngadd  46883  2zrngmul  46891