Theorem rabex2 5276

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3390  Vcvv 3430

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rab2ex  5277  mapfien2  9313  cantnffval  9573  nqex  10835  gsumvalx  18602  psgnfval  19433  odval  19467  sylow1lem2  19532  sylow3lem6  19565  ablfaclem1  20020  psrass1lem  21889  psrbas  21890  psrelbas  21891  psrmulfval  21900  psrmulcllem  21902  psrvscaval  21907  psr0cl  21909  psr0lid  21910  psrnegcl  21911  psrlinv  21912  psr1cl  21917  psrlidm  21918  psrdi  21921  psrdir  21922  psrass23l  21923  psrcom  21924  psrass23  21925  mvrval  21938  mplsubglem  21955  mpllsslem  21956  mplsubrglem  21960  mplvscaval  21972  mplmon  21991  mplmonmul  21992  mplcoe1  21993  ltbval  21999  mplmon2  22017  evlslem2  22035  evlslem3  22036  evlslem1  22038  evlsvvvallem2  22048  psdval  22103  rrxmet  25353  mdegldg  26012  lgamgulmlem5  26983  lgamgulmlem6  26984  lgamgulm2  26986  lgamcvglem  26990  upgrres1lem1  29366  frgrwopreg1  30377  dlwwlknondlwlknonen  30425  nsgmgc  33477  nsgqusf1o  33481  ssdifidl  33522  extvfv  33682  extvfvcl  33685  extvfvalf  33686  psrgsum  33697  psrmon  33698  psrmonmul  33699  psrmonmul2  33700  psrmonprod  33701  mplmonprod  33703  issply  33710  esplyfval2  33714  esplympl  33716  esplyfv  33719  esplyfval3  33721  esplyind  33724  eulerpartlem1  34517  eulerpartlemt  34521  eulerpartgbij  34522  ballotlemoex  34636  satffunlem2lem2  35594  mapdunirnN  42087  mplmapghm  42996  selvvvval  43017  evlsmhpvvval  43027  pwfi2en  43528  smfresal  47220  oddiadd  48608  2zrngadd  48677  2zrngmul  48685