Theorem rabex2 5269

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  {crab 3391  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-pw 4531

This theorem is referenced by:  rab2ex  5270  mapfien2  9312  cantnffval  9575  nqex  10837  gsumvalx  18635  psgnfval  19466  odval  19500  sylow1lem2  19565  sylow3lem6  19598  ablfaclem1  20053  psrass1lem  21908  psrbas  21909  psrelbas  21910  psrmulfval  21918  psrmulcllem  21920  psrvscaval  21925  psr0cl  21927  psr0lid  21928  psrnegcl  21929  psrlinv  21930  psr1cl  21935  psrlidm  21936  psrdi  21939  psrdir  21940  psrass23l  21941  psrcom  21942  psrass23  21943  mvrval  21956  mplsubglem  21973  mpllsslem  21974  mplsubrglem  21978  mplvscaval  21990  mplmon  22011  mplmonmul  22012  mplcoe1  22013  ltbval  22019  mplmon2  22037  evlslem2  22055  evlslem3  22056  evlslem1  22058  evlsvvvallem2  22068  mplmapghm  22098  selvvvval  22118  psdval  22147  rrxmet  25393  mdegldg  26049  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvglem  27021  upgrres1lem1  29396  frgrwopreg1  30406  dlwwlknondlwlknonen  30454  nsgmgc  33495  nsgqusf1o  33499  ssdifidl  33540  extvfv  33717  extvfvcl  33720  extvfvalf  33721  psrgsum  33732  psrmon  33733  psrmonmul  33734  psrmonmul2  33735  psrmonprod  33736  mplmonprod  33738  issply  33745  esplyfval2  33749  esplympl  33751  esplyfv  33754  esplyfval3  33756  esplyind  33759  eulerpartlem1  34551  eulerpartlemt  34555  eulerpartgbij  34556  ballotlemoex  34670  satffunlem2lem2  35634  mapdunirnN  42142  evlsmhpvvval  43045  pwfi2en  43542  smfresal  47231  oddiadd  48665  2zrngadd  48734  2zrngmul  48742