Theorem rabex2 5253

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  {crab 3067  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rab2ex  5254  mapfien2  9098  cantnffval  9351  nqex  10610  gsumvalx  18275  psgnfval  19023  odval  19057  sylow1lem2  19119  sylow3lem6  19152  ablfaclem1  19603  psrass1lemOLD  21053  psrass1lem  21056  psrbas  21057  psrelbas  21058  psrmulfval  21064  psrmulcllem  21066  psrvscaval  21071  psr0cl  21073  psr0lid  21074  psrnegcl  21075  psrlinv  21076  psr1cl  21081  psrlidm  21082  psrdi  21085  psrdir  21086  psrass23l  21087  psrcom  21088  psrass23  21089  mvrval  21100  mplsubglem  21115  mpllsslem  21116  mplsubrglem  21120  mplvscaval  21130  mplmon  21146  mplmonmul  21147  mplcoe1  21148  ltbval  21154  mplmon2  21179  evlslem2  21199  evlslem3  21200  evlslem1  21202  rrxmet  24477  mdegldg  25136  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgamcvglem  26094  upgrres1lem1  27579  frgrwopreg1  28583  dlwwlknondlwlknonen  28631  nsgmgc  31499  nsgqusf1o  31503  eulerpartlem1  32234  eulerpartlemt  32238  eulerpartgbij  32239  ballotlemoex  32352  satffunlem2lem2  33268  mapdunirnN  39591  pwfi2en  40838  smfresal  44209  oddiadd  45256  2zrngadd  45383  2zrngmul  45391