Theorem rabex2 5258

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  {crab 3068  Vcvv 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  rab2ex  5259  mapfien2  9168  cantnffval  9421  nqex  10679  gsumvalx  18360  psgnfval  19108  odval  19142  sylow1lem2  19204  sylow3lem6  19237  ablfaclem1  19688  psrass1lemOLD  21143  psrass1lem  21146  psrbas  21147  psrelbas  21148  psrmulfval  21154  psrmulcllem  21156  psrvscaval  21161  psr0cl  21163  psr0lid  21164  psrnegcl  21165  psrlinv  21166  psr1cl  21171  psrlidm  21172  psrdi  21175  psrdir  21176  psrass23l  21177  psrcom  21178  psrass23  21179  mvrval  21190  mplsubglem  21205  mpllsslem  21206  mplsubrglem  21210  mplvscaval  21220  mplmon  21236  mplmonmul  21237  mplcoe1  21238  ltbval  21244  mplmon2  21269  evlslem2  21289  evlslem3  21290  evlslem1  21292  rrxmet  24572  mdegldg  25231  lgamgulmlem5  26182  lgamgulmlem6  26183  lgamgulm2  26185  lgamcvglem  26189  upgrres1lem1  27676  frgrwopreg1  28682  dlwwlknondlwlknonen  28730  nsgmgc  31597  nsgqusf1o  31601  eulerpartlem1  32334  eulerpartlemt  32338  eulerpartgbij  32339  ballotlemoex  32452  satffunlem2lem2  33368  mapdunirnN  39664  pwfi2en  40922  smfresal  44322  oddiadd  45368  2zrngadd  45495  2zrngmul  45503