Theorem rabex2 5359

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  {crab 3443  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  rab2ex  5360  mapfien2  9478  cantnffval  9732  nqex  10992  gsumvalx  18714  psgnfval  19542  odval  19576  sylow1lem2  19641  sylow3lem6  19674  ablfaclem1  20129  psrass1lem  21975  psrbas  21976  psrelbas  21977  psrmulfval  21986  psrmulcllem  21988  psrvscaval  21993  psr0cl  21995  psr0lid  21996  psrnegcl  21997  psrlinv  21998  psr1cl  22004  psrlidm  22005  psrdi  22008  psrdir  22009  psrass23l  22010  psrcom  22011  psrass23  22012  mvrval  22025  mplsubglem  22042  mpllsslem  22043  mplsubrglem  22047  mplvscaval  22059  mplmon  22076  mplmonmul  22077  mplcoe1  22078  ltbval  22084  mplmon2  22108  evlslem2  22126  evlslem3  22127  evlslem1  22129  psdval  22186  rrxmet  25461  mdegldg  26125  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamcvglem  27101  upgrres1lem1  29344  frgrwopreg1  30350  dlwwlknondlwlknonen  30398  nsgmgc  33405  nsgqusf1o  33409  ssdifidl  33450  eulerpartlem1  34332  eulerpartlemt  34336  eulerpartgbij  34337  ballotlemoex  34450  satffunlem2lem2  35374  mapdunirnN  41607  mplmapghm  42511  evlsvvvallem2  42517  selvvvval  42540  evlsmhpvvval  42550  pwfi2en  43054  smfresal  46709  oddiadd  47897  2zrngadd  47966  2zrngmul  47974