Theorem rabex2 5296

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  {crab 3405  Vcvv 3446

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 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  rab2ex  5297  mapfien2  9354  cantnffval  9608  nqex  10868  gsumvalx  18545  psgnfval  19296  odval  19330  sylow1lem2  19395  sylow3lem6  19428  ablfaclem1  19878  psrass1lemOLD  21379  psrass1lem  21382  psrbas  21383  psrelbas  21384  psrmulfval  21390  psrmulcllem  21392  psrvscaval  21397  psr0cl  21399  psr0lid  21400  psrnegcl  21401  psrlinv  21402  psr1cl  21408  psrlidm  21409  psrdi  21412  psrdir  21413  psrass23l  21414  psrcom  21415  psrass23  21416  mvrval  21427  mplsubglem  21442  mpllsslem  21443  mplsubrglem  21447  mplvscaval  21457  mplmon  21473  mplmonmul  21474  mplcoe1  21475  ltbval  21481  mplmon2  21506  evlslem2  21526  evlslem3  21527  evlslem1  21529  rrxmet  24809  mdegldg  25468  lgamgulmlem5  26419  lgamgulmlem6  26420  lgamgulm2  26422  lgamcvglem  26426  upgrres1lem1  28320  frgrwopreg1  29325  dlwwlknondlwlknonen  29373  nsgmgc  32264  nsgqusf1o  32268  eulerpartlem1  33056  eulerpartlemt  33060  eulerpartgbij  33061  ballotlemoex  33174  satffunlem2lem2  34087  mapdunirnN  40186  pwfi2en  41482  smfresal  45149  oddiadd  46228  2zrngadd  46355  2zrngmul  46363