Theorem rabex2 5201

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  rab2ex  5202  mapfien2  8856  cantnffval  9110  nqex  10334  gsumvalx  17878  psgnfval  18620  odval  18654  sylow1lem2  18716  sylow3lem6  18749  ablfaclem1  19200  psrass1lem  20615  psrbas  20616  psrelbas  20617  psrmulfval  20623  psrmulcllem  20625  psrvscaval  20630  psr0cl  20632  psr0lid  20633  psrnegcl  20634  psrlinv  20635  psr1cl  20640  psrlidm  20641  psrdi  20644  psrdir  20645  psrass23l  20646  psrcom  20647  psrass23  20648  mvrval  20659  mplsubglem  20672  mpllsslem  20673  mplsubrglem  20677  mplvscaval  20687  mplmon  20703  mplmonmul  20704  mplcoe1  20705  ltbval  20711  opsrtoslem2  20724  mplmon2  20732  evlslem2  20751  evlslem3  20752  evlslem1  20754  rrxmet  24012  mdegldg  24667  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgamcvglem  25625  upgrres1lem1  27099  frgrwopreg1  28103  dlwwlknondlwlknonen  28151  eulerpartlem1  31735  eulerpartlemt  31739  eulerpartgbij  31740  ballotlemoex  31853  satffunlem2lem2  32766  mapdunirnN  38946  pwfi2en  40041  smfresal  43420  oddiadd  44434  2zrngadd  44561  2zrngmul  44569