Theorem rabex2 5212

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3058  Vcvv 3400

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5177

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402  df-in 3860  df-ss 3870

This theorem is referenced by:  rab2ex  5213  mapfien2  8959  cantnffval  9212  nqex  10436  gsumvalx  18015  psgnfval  18759  odval  18793  sylow1lem2  18855  sylow3lem6  18888  ablfaclem1  19339  psrass1lemOLD  20766  psrass1lem  20769  psrbas  20770  psrelbas  20771  psrmulfval  20777  psrmulcllem  20779  psrvscaval  20784  psr0cl  20786  psr0lid  20787  psrnegcl  20788  psrlinv  20789  psr1cl  20794  psrlidm  20795  psrdi  20798  psrdir  20799  psrass23l  20800  psrcom  20801  psrass23  20802  mvrval  20813  mplsubglem  20828  mpllsslem  20829  mplsubrglem  20833  mplvscaval  20843  mplmon  20859  mplmonmul  20860  mplcoe1  20861  ltbval  20867  mplmon2  20886  evlslem2  20906  evlslem3  20907  evlslem1  20909  rrxmet  24173  mdegldg  24832  lgamgulmlem5  25783  lgamgulmlem6  25784  lgamgulm2  25786  lgamcvglem  25790  upgrres1lem1  27264  frgrwopreg1  28268  dlwwlknondlwlknonen  28316  nsgmgc  31182  nsgqusf1o  31186  eulerpartlem1  31917  eulerpartlemt  31921  eulerpartgbij  31922  ballotlemoex  32035  satffunlem2lem2  32952  mapdunirnN  39320  pwfi2en  40535  smfresal  43902  oddiadd  44950  2zrngadd  45077  2zrngmul  45085