Theorem rabex2 5291

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3402  Vcvv 3444

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rab2ex  5292  mapfien2  9336  cantnffval  9592  nqex  10852  gsumvalx  18579  psgnfval  19406  odval  19440  sylow1lem2  19505  sylow3lem6  19538  ablfaclem1  19993  psrass1lem  21817  psrbas  21818  psrelbas  21819  psrmulfval  21828  psrmulcllem  21830  psrvscaval  21835  psr0cl  21837  psr0lid  21838  psrnegcl  21839  psrlinv  21840  psr1cl  21846  psrlidm  21847  psrdi  21850  psrdir  21851  psrass23l  21852  psrcom  21853  psrass23  21854  mvrval  21867  mplsubglem  21884  mpllsslem  21885  mplsubrglem  21889  mplvscaval  21901  mplmon  21918  mplmonmul  21919  mplcoe1  21920  ltbval  21926  mplmon2  21944  evlslem2  21962  evlslem3  21963  evlslem1  21965  psdval  22022  rrxmet  25284  mdegldg  25947  lgamgulmlem5  26919  lgamgulmlem6  26920  lgamgulm2  26922  lgamcvglem  26926  upgrres1lem1  29212  frgrwopreg1  30220  dlwwlknondlwlknonen  30268  nsgmgc  33356  nsgqusf1o  33360  ssdifidl  33401  eulerpartlem1  34331  eulerpartlemt  34335  eulerpartgbij  34336  ballotlemoex  34450  satffunlem2lem2  35366  mapdunirnN  41617  mplmapghm  42517  evlsvvvallem2  42523  selvvvval  42546  evlsmhpvvval  42556  pwfi2en  43059  smfresal  46759  oddiadd  48135  2zrngadd  48204  2zrngmul  48212