Theorem rabex2 5299

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3408  Vcvv 3450

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  rab2ex  5300  mapfien2  9367  cantnffval  9623  nqex  10883  gsumvalx  18610  psgnfval  19437  odval  19471  sylow1lem2  19536  sylow3lem6  19569  ablfaclem1  20024  psrass1lem  21848  psrbas  21849  psrelbas  21850  psrmulfval  21859  psrmulcllem  21861  psrvscaval  21866  psr0cl  21868  psr0lid  21869  psrnegcl  21870  psrlinv  21871  psr1cl  21877  psrlidm  21878  psrdi  21881  psrdir  21882  psrass23l  21883  psrcom  21884  psrass23  21885  mvrval  21898  mplsubglem  21915  mpllsslem  21916  mplsubrglem  21920  mplvscaval  21932  mplmon  21949  mplmonmul  21950  mplcoe1  21951  ltbval  21957  mplmon2  21975  evlslem2  21993  evlslem3  21994  evlslem1  21996  psdval  22053  rrxmet  25315  mdegldg  25978  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamcvglem  26957  upgrres1lem1  29243  frgrwopreg1  30254  dlwwlknondlwlknonen  30302  nsgmgc  33390  nsgqusf1o  33394  ssdifidl  33435  eulerpartlem1  34365  eulerpartlemt  34369  eulerpartgbij  34370  ballotlemoex  34484  satffunlem2lem2  35400  mapdunirnN  41651  mplmapghm  42551  evlsvvvallem2  42557  selvvvval  42580  evlsmhpvvval  42590  pwfi2en  43093  smfresal  46793  oddiadd  48166  2zrngadd  48235  2zrngmul  48243