Theorem rabex2 5311

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3415  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  rab2ex  5312  mapfien2  9421  cantnffval  9677  nqex  10937  gsumvalx  18654  psgnfval  19481  odval  19515  sylow1lem2  19580  sylow3lem6  19613  ablfaclem1  20068  psrass1lem  21892  psrbas  21893  psrelbas  21894  psrmulfval  21903  psrmulcllem  21905  psrvscaval  21910  psr0cl  21912  psr0lid  21913  psrnegcl  21914  psrlinv  21915  psr1cl  21921  psrlidm  21922  psrdi  21925  psrdir  21926  psrass23l  21927  psrcom  21928  psrass23  21929  mvrval  21942  mplsubglem  21959  mpllsslem  21960  mplsubrglem  21964  mplvscaval  21976  mplmon  21993  mplmonmul  21994  mplcoe1  21995  ltbval  22001  mplmon2  22019  evlslem2  22037  evlslem3  22038  evlslem1  22040  psdval  22097  rrxmet  25360  mdegldg  26023  lgamgulmlem5  26995  lgamgulmlem6  26996  lgamgulm2  26998  lgamcvglem  27002  upgrres1lem1  29288  frgrwopreg1  30299  dlwwlknondlwlknonen  30347  nsgmgc  33427  nsgqusf1o  33431  ssdifidl  33472  eulerpartlem1  34399  eulerpartlemt  34403  eulerpartgbij  34404  ballotlemoex  34518  satffunlem2lem2  35428  mapdunirnN  41669  mplmapghm  42579  evlsvvvallem2  42585  selvvvval  42608  evlsmhpvvval  42618  pwfi2en  43121  smfresal  46817  oddiadd  48149  2zrngadd  48218  2zrngmul  48226