Theorem rabex2 5297

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  {crab 3414  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-in 3911  df-ss 3921  df-pw 4557

This theorem is referenced by:  rab2ex  5298  mapfien2  9355  cantnffval  9618  nqex  10881  gsumvalx  18710  psgnfval  19540  odval  19574  sylow1lem2  19639  sylow3lem6  19672  ablfaclem1  20127  psrass1lem  21982  psrbas  21983  psrelbas  21984  psrmulfval  21992  psrmulcllem  21994  psrvscaval  21999  psr0cl  22001  psr0lid  22002  psrnegcl  22003  psrlinv  22004  psr1cl  22009  psrlidm  22010  psrdi  22013  psrdir  22014  psrass23l  22015  psrcom  22016  psrass23  22017  mvrval  22030  mplsubglem  22047  mpllsslem  22048  mplsubrglem  22052  mplvscaval  22064  mplmon  22085  mplmonmul  22086  mplcoe1  22087  ltbval  22093  mplmon2  22111  evlslem2  22129  evlslem3  22130  evlslem1  22132  evlsvvvallem2  22142  mplmapghm  22172  selvvvval  22192  psdval  22221  rrxmet  25467  mdegldg  26123  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamcvglem  27101  upgrres1lem1  29507  frgrwopreg1  30517  dlwwlknondlwlknonen  30565  nsgmgc  33595  nsgqusf1o  33599  ssdifidl  33641  extvfv  33827  extvfvcl  33830  extvfvalf  33831  psrgsum  33842  psrmon  33843  psrmonmul  33844  psrmonmul2  33845  psrmonprod  33846  mplmonprod  33848  issply  33855  esplyfval2  33859  esplympl  33861  esplyfv  33864  esplyfval3  33866  esplyind  33869  eulerpartlem1  34661  eulerpartlemt  34665  eulerpartgbij  34666  ballotlemoex  34780  satffunlem2lem2  35753  mapdunirnN  42271  evlsmhpvvval  43174  pwfi2en  43671  smfresal  47359  oddiadd  48793  2zrngadd  48862  2zrngmul  48870