Theorem rabex2 5277

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  {crab 3395  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549

This theorem is referenced by:  rab2ex  5278  mapfien2  9293  cantnffval  9553  nqex  10814  gsumvalx  18584  psgnfval  19412  odval  19446  sylow1lem2  19511  sylow3lem6  19544  ablfaclem1  19999  psrass1lem  21869  psrbas  21870  psrelbas  21871  psrmulfval  21880  psrmulcllem  21882  psrvscaval  21887  psr0cl  21889  psr0lid  21890  psrnegcl  21891  psrlinv  21892  psr1cl  21898  psrlidm  21899  psrdi  21902  psrdir  21903  psrass23l  21904  psrcom  21905  psrass23  21906  mvrval  21919  mplsubglem  21936  mpllsslem  21937  mplsubrglem  21941  mplvscaval  21953  mplmon  21970  mplmonmul  21971  mplcoe1  21972  ltbval  21978  mplmon2  21996  evlslem2  22014  evlslem3  22015  evlslem1  22017  psdval  22074  rrxmet  25335  mdegldg  25998  lgamgulmlem5  26970  lgamgulmlem6  26971  lgamgulm2  26973  lgamcvglem  26977  upgrres1lem1  29287  frgrwopreg1  30298  dlwwlknondlwlknonen  30346  nsgmgc  33377  nsgqusf1o  33381  ssdifidl  33422  issply  33584  esplympl  33588  esplyfv  33591  eulerpartlem1  34380  eulerpartlemt  34384  eulerpartgbij  34385  ballotlemoex  34499  satffunlem2lem2  35450  mapdunirnN  41697  mplmapghm  42597  evlsvvvallem2  42603  selvvvval  42626  evlsmhpvvval  42636  pwfi2en  43138  smfresal  46834  oddiadd  48213  2zrngadd  48282  2zrngmul  48290