Theorem rabex2 5282

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3389  Vcvv 3429

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 2708  ax-sep 5231

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  rab2ex  5283  mapfien2  9322  cantnffval  9584  nqex  10846  gsumvalx  18644  psgnfval  19475  odval  19509  sylow1lem2  19574  sylow3lem6  19607  ablfaclem1  20062  psrass1lem  21912  psrbas  21913  psrelbas  21914  psrmulfval  21922  psrmulcllem  21924  psrvscaval  21929  psr0cl  21931  psr0lid  21932  psrnegcl  21933  psrlinv  21934  psr1cl  21939  psrlidm  21940  psrdi  21943  psrdir  21944  psrass23l  21945  psrcom  21946  psrass23  21947  mvrval  21960  mplsubglem  21977  mpllsslem  21978  mplsubrglem  21982  mplvscaval  21994  mplmon  22013  mplmonmul  22014  mplcoe1  22015  ltbval  22021  mplmon2  22039  evlslem2  22057  evlslem3  22058  evlslem1  22060  evlsvvvallem2  22070  psdval  22125  rrxmet  25375  mdegldg  26031  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamcvglem  27003  upgrres1lem1  29378  frgrwopreg1  30388  dlwwlknondlwlknonen  30436  nsgmgc  33472  nsgqusf1o  33476  ssdifidl  33517  extvfv  33677  extvfvcl  33680  extvfvalf  33681  psrgsum  33692  psrmon  33693  psrmonmul  33694  psrmonmul2  33695  psrmonprod  33696  mplmonprod  33698  issply  33705  esplyfval2  33709  esplympl  33711  esplyfv  33714  esplyfval3  33716  esplyind  33719  eulerpartlem1  34511  eulerpartlemt  34515  eulerpartgbij  34516  ballotlemoex  34630  satffunlem2lem2  35588  mapdunirnN  42096  mplmapghm  42997  selvvvval  43018  evlsmhpvvval  43028  pwfi2en  43525  smfresal  47216  oddiadd  48650  2zrngadd  48719  2zrngmul  48727