Theorem rabex2 5341

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3436  Vcvv 3480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  rab2ex  5342  mapfien2  9449  cantnffval  9703  nqex  10963  gsumvalx  18689  psgnfval  19518  odval  19552  sylow1lem2  19617  sylow3lem6  19650  ablfaclem1  20105  psrass1lem  21952  psrbas  21953  psrelbas  21954  psrmulfval  21963  psrmulcllem  21965  psrvscaval  21970  psr0cl  21972  psr0lid  21973  psrnegcl  21974  psrlinv  21975  psr1cl  21981  psrlidm  21982  psrdi  21985  psrdir  21986  psrass23l  21987  psrcom  21988  psrass23  21989  mvrval  22002  mplsubglem  22019  mpllsslem  22020  mplsubrglem  22024  mplvscaval  22036  mplmon  22053  mplmonmul  22054  mplcoe1  22055  ltbval  22061  mplmon2  22085  evlslem2  22103  evlslem3  22104  evlslem1  22106  psdval  22163  rrxmet  25442  mdegldg  26105  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvglem  27083  upgrres1lem1  29326  frgrwopreg1  30337  dlwwlknondlwlknonen  30385  nsgmgc  33440  nsgqusf1o  33444  ssdifidl  33485  eulerpartlem1  34369  eulerpartlemt  34373  eulerpartgbij  34374  ballotlemoex  34488  satffunlem2lem2  35411  mapdunirnN  41652  mplmapghm  42566  evlsvvvallem2  42572  selvvvval  42595  evlsmhpvvval  42605  pwfi2en  43109  smfresal  46803  oddiadd  48090  2zrngadd  48159  2zrngmul  48167