Theorem rabex2 5288

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 5287	. 2 ⊢ (𝐴 ∈ V → 𝐵 ∈ V)
5	1, 4	ax-mp 5	1 ⊢ 𝐵 ∈ V

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3401  Vcvv 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  rab2ex  5289  mapfien2  9324  cantnffval  9584  nqex  10846  gsumvalx  18613  psgnfval  19441  odval  19475  sylow1lem2  19540  sylow3lem6  19573  ablfaclem1  20028  psrass1lem  21900  psrbas  21901  psrelbas  21902  psrmulfval  21911  psrmulcllem  21913  psrvscaval  21918  psr0cl  21920  psr0lid  21921  psrnegcl  21922  psrlinv  21923  psr1cl  21928  psrlidm  21929  psrdi  21932  psrdir  21933  psrass23l  21934  psrcom  21935  psrass23  21936  mvrval  21949  mplsubglem  21966  mpllsslem  21967  mplsubrglem  21971  mplvscaval  21983  mplmon  22002  mplmonmul  22003  mplcoe1  22004  ltbval  22010  mplmon2  22028  evlslem2  22046  evlslem3  22047  evlslem1  22049  evlsvvvallem2  22059  psdval  22114  rrxmet  25376  mdegldg  26039  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvglem  27018  upgrres1lem1  29394  frgrwopreg1  30405  dlwwlknondlwlknonen  30453  nsgmgc  33505  nsgqusf1o  33509  ssdifidl  33550  extvfv  33710  extvfvcl  33713  extvfvalf  33714  psrgsum  33725  psrmon  33726  psrmonmul  33727  psrmonmul2  33728  psrmonprod  33729  mplmonprod  33731  issply  33738  esplyfval2  33742  esplympl  33744  esplyfv  33747  esplyfval3  33749  esplyind  33752  eulerpartlem1  34545  eulerpartlemt  34549  eulerpartgbij  34550  ballotlemoex  34664  satffunlem2lem2  35622  mapdunirnN  42026  mplmapghm  42922  selvvvval  42943  evlsmhpvvval  42953  pwfi2en  43454  smfresal  47146  oddiadd  48534  2zrngadd  48603  2zrngmul  48611