Theorem rabex2 5284

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3397  Vcvv 3438

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 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-pw 4554

This theorem is referenced by:  rab2ex  5285  mapfien2  9310  cantnffval  9570  nqex  10832  gsumvalx  18599  psgnfval  19427  odval  19461  sylow1lem2  19526  sylow3lem6  19559  ablfaclem1  20014  psrass1lem  21886  psrbas  21887  psrelbas  21888  psrmulfval  21897  psrmulcllem  21899  psrvscaval  21904  psr0cl  21906  psr0lid  21907  psrnegcl  21908  psrlinv  21909  psr1cl  21914  psrlidm  21915  psrdi  21918  psrdir  21919  psrass23l  21920  psrcom  21921  psrass23  21922  mvrval  21935  mplsubglem  21952  mpllsslem  21953  mplsubrglem  21957  mplvscaval  21969  mplmon  21988  mplmonmul  21989  mplcoe1  21990  ltbval  21996  mplmon2  22014  evlslem2  22032  evlslem3  22033  evlslem1  22035  evlsvvvallem2  22045  psdval  22100  rrxmet  25362  mdegldg  26025  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgamcvglem  27004  upgrres1lem1  29331  frgrwopreg1  30342  dlwwlknondlwlknonen  30390  nsgmgc  33442  nsgqusf1o  33446  ssdifidl  33487  extvfv  33647  extvfvcl  33650  extvfvalf  33651  issply  33668  esplyfval2  33672  esplympl  33674  esplyfv  33677  esplyfval3  33679  esplyind  33680  eulerpartlem1  34473  eulerpartlemt  34477  eulerpartgbij  34478  ballotlemoex  34592  satffunlem2lem2  35549  mapdunirnN  41849  mplmapghm  42749  selvvvval  42770  evlsmhpvvval  42780  pwfi2en  43281  smfresal  46974  oddiadd  48362  2zrngadd  48431  2zrngmul  48439