Theorem rabex2 5311

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  {crab 3416  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3912  df-ss 3922  df-pw 4564

This theorem is referenced by:  rab2ex  5312  mapfien2  9365  cantnffval  9628  nqex  10903  gsumvalx  18729  psgnfval  19565  odval  19599  sylow1lem2  19664  sylow3lem6  19697  ablfaclem1  20152  ssdifidl  21485  psrass1lem  22083  psrbas  22084  psrelbas  22085  psrmulfval  22093  psrmulcllem  22095  psrvscaval  22100  psr0cl  22102  psr0lid  22103  psrnegcl  22104  psrlinv  22105  psr1cl  22110  psrlidm  22111  psrdi  22114  psrdir  22115  psrass23l  22116  psrcom  22117  psrass23  22118  mvrval  22131  mplsubglem  22148  mpllsslem  22149  mplsubrglem  22153  mplvscaval  22165  mplmon  22186  mplmonmul  22187  mplcoe1  22188  ltbval  22194  mplmon2  22212  evlslem2  22230  evlslem3  22231  evlslem1  22233  evlsvvvallem2  22243  mplmapghm  22273  selvvvval  22293  psdval  22322  rrxmet  25567  mdegldg  26223  lgamgulmlem5  27197  lgamgulmlem6  27198  lgamgulm2  27200  lgamcvglem  27204  upgrres1lem1  29659  frgrwopreg1  30669  dlwwlknondlwlknonen  30717  nsgmgc  33721  nsgqusf1o  33725  extvfv  33923  extvfvcl  33926  extvfvalf  33927  psrgsum  33938  psrmon  33939  psrmonmul  33940  psrmonmul2  33941  psrmonprod  33942  mplmonprod  33944  issply  33951  esplyfval2  33955  esplympl  33957  esplyfv  33960  esplyfval3  33962  esplyind  33965  eulerpartlem1  34757  eulerpartlemt  34761  eulerpartgbij  34762  ballotlemoex  34876  satffunlem2lem2  35898  mapdunirnN  42424  evlsmhpvvval  43327  pwfi2en  43824  smfresal  47502  oddiadd  48939  2zrngadd  49008  2zrngmul  49016