Theorem rabex2 5312

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  {crab 3423  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-in 3920  df-ss 3930  df-pw 4569

This theorem is referenced by:  rab2ex  5313  mapfien2  9368  cantnffval  9631  nqex  10907  gsumvalx  18733  psgnfval  19569  odval  19603  sylow1lem2  19668  sylow3lem6  19701  ablfaclem1  20156  ssdifidl  21453  psrass1lem  22051  psrbas  22052  psrelbas  22053  psrmulfval  22061  psrmulcllem  22063  psrvscaval  22068  psr0cl  22070  psr0lid  22071  psrnegcl  22072  psrlinv  22073  psr1cl  22078  psrlidm  22079  psrdi  22082  psrdir  22083  psrass23l  22084  psrcom  22085  psrass23  22086  mvrval  22099  mplsubglem  22116  mpllsslem  22117  mplsubrglem  22121  mplvscaval  22133  mplmon  22154  mplmonmul  22155  mplcoe1  22156  ltbval  22162  mplmon2  22180  evlslem2  22198  evlslem3  22199  evlslem1  22201  evlsvvvallem2  22211  mplmapghm  22241  selvvvval  22261  psdval  22290  rrxmet  25535  mdegldg  26191  lgamgulmlem5  27162  lgamgulmlem6  27163  lgamgulm2  27165  lgamcvglem  27169  upgrres1lem1  29599  frgrwopreg1  30609  dlwwlknondlwlknonen  30657  nsgmgc  33664  nsgqusf1o  33668  extvfv  33867  extvfvcl  33870  extvfvalf  33871  psrgsum  33882  psrmon  33883  psrmonmul  33884  psrmonmul2  33885  psrmonprod  33886  mplmonprod  33888  issply  33895  esplyfval2  33899  esplympl  33901  esplyfv  33904  esplyfval3  33906  esplyind  33909  eulerpartlem1  34701  eulerpartlemt  34705  eulerpartgbij  34706  ballotlemoex  34820  satffunlem2lem2  35796  mapdunirnN  42313  evlsmhpvvval  43218  pwfi2en  43715  smfresal  47393  oddiadd  48827  2zrngadd  48896  2zrngmul  48904