Theorem rabex2 5334

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  {crab 3432  Vcvv 3474

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  rab2ex  5335  mapfien2  9406  cantnffval  9660  nqex  10920  gsumvalx  18601  psgnfval  19409  odval  19443  sylow1lem2  19508  sylow3lem6  19541  ablfaclem1  19996  psrass1lemOLD  21712  psrass1lem  21715  psrbas  21716  psrelbas  21717  psrmulfval  21723  psrmulcllem  21725  psrvscaval  21730  psr0cl  21732  psr0lid  21733  psrnegcl  21734  psrlinv  21735  psr1cl  21741  psrlidm  21742  psrdi  21745  psrdir  21746  psrass23l  21747  psrcom  21748  psrass23  21749  mvrval  21760  mplsubglem  21777  mpllsslem  21778  mplsubrglem  21782  mplvscaval  21794  mplmon  21809  mplmonmul  21810  mplcoe1  21811  ltbval  21817  mplmon2  21841  evlslem2  21861  evlslem3  21862  evlslem1  21864  rrxmet  25149  mdegldg  25808  lgamgulmlem5  26761  lgamgulmlem6  26762  lgamgulm2  26764  lgamcvglem  26768  upgrres1lem1  28821  frgrwopreg1  29826  dlwwlknondlwlknonen  29874  nsgmgc  32785  nsgqusf1o  32789  eulerpartlem1  33652  eulerpartlemt  33656  eulerpartgbij  33657  ballotlemoex  33770  satffunlem2lem2  34683  mapdunirnN  40824  mplmapghm  41430  evlsvvvallem2  41436  selvvvval  41459  evlsmhpvvval  41469  pwfi2en  42141  smfresal  45803  oddiadd  46851  2zrngadd  46924  2zrngmul  46932