Theorem rabex2 5296

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3405  Vcvv 3447

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 5251

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 3406  df-v 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  rab2ex  5297  mapfien2  9360  cantnffval  9616  nqex  10876  gsumvalx  18603  psgnfval  19430  odval  19464  sylow1lem2  19529  sylow3lem6  19562  ablfaclem1  20017  psrass1lem  21841  psrbas  21842  psrelbas  21843  psrmulfval  21852  psrmulcllem  21854  psrvscaval  21859  psr0cl  21861  psr0lid  21862  psrnegcl  21863  psrlinv  21864  psr1cl  21870  psrlidm  21871  psrdi  21874  psrdir  21875  psrass23l  21876  psrcom  21877  psrass23  21878  mvrval  21891  mplsubglem  21908  mpllsslem  21909  mplsubrglem  21913  mplvscaval  21925  mplmon  21942  mplmonmul  21943  mplcoe1  21944  ltbval  21950  mplmon2  21968  evlslem2  21986  evlslem3  21987  evlslem1  21989  psdval  22046  rrxmet  25308  mdegldg  25971  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvglem  26950  upgrres1lem1  29236  frgrwopreg1  30247  dlwwlknondlwlknonen  30295  nsgmgc  33383  nsgqusf1o  33387  ssdifidl  33428  eulerpartlem1  34358  eulerpartlemt  34362  eulerpartgbij  34363  ballotlemoex  34477  satffunlem2lem2  35393  mapdunirnN  41644  mplmapghm  42544  evlsvvvallem2  42550  selvvvval  42573  evlsmhpvvval  42583  pwfi2en  43086  smfresal  46786  oddiadd  48162  2zrngadd  48231  2zrngmul  48239