Theorem rabex2 5280

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3394  Vcvv 3436

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  rab2ex  5281  mapfien2  9299  cantnffval  9559  nqex  10817  gsumvalx  18550  psgnfval  19379  odval  19413  sylow1lem2  19478  sylow3lem6  19511  ablfaclem1  19966  psrass1lem  21839  psrbas  21840  psrelbas  21841  psrmulfval  21850  psrmulcllem  21852  psrvscaval  21857  psr0cl  21859  psr0lid  21860  psrnegcl  21861  psrlinv  21862  psr1cl  21868  psrlidm  21869  psrdi  21872  psrdir  21873  psrass23l  21874  psrcom  21875  psrass23  21876  mvrval  21889  mplsubglem  21906  mpllsslem  21907  mplsubrglem  21911  mplvscaval  21923  mplmon  21940  mplmonmul  21941  mplcoe1  21942  ltbval  21948  mplmon2  21966  evlslem2  21984  evlslem3  21985  evlslem1  21987  psdval  22044  rrxmet  25306  mdegldg  25969  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgamcvglem  26948  upgrres1lem1  29254  frgrwopreg1  30262  dlwwlknondlwlknonen  30310  nsgmgc  33349  nsgqusf1o  33353  ssdifidl  33394  eulerpartlem1  34335  eulerpartlemt  34339  eulerpartgbij  34340  ballotlemoex  34454  satffunlem2lem2  35379  mapdunirnN  41629  mplmapghm  42529  evlsvvvallem2  42535  selvvvval  42558  evlsmhpvvval  42568  pwfi2en  43070  smfresal  46769  oddiadd  48158  2zrngadd  48227  2zrngmul  48235