Theorem rabex2 5286

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3399  Vcvv 3440

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 2708  ax-sep 5241

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  rab2ex  5287  mapfien2  9312  cantnffval  9572  nqex  10834  gsumvalx  18601  psgnfval  19429  odval  19463  sylow1lem2  19528  sylow3lem6  19561  ablfaclem1  20016  psrass1lem  21888  psrbas  21889  psrelbas  21890  psrmulfval  21899  psrmulcllem  21901  psrvscaval  21906  psr0cl  21908  psr0lid  21909  psrnegcl  21910  psrlinv  21911  psr1cl  21916  psrlidm  21917  psrdi  21920  psrdir  21921  psrass23l  21922  psrcom  21923  psrass23  21924  mvrval  21937  mplsubglem  21954  mpllsslem  21955  mplsubrglem  21959  mplvscaval  21971  mplmon  21990  mplmonmul  21991  mplcoe1  21992  ltbval  21998  mplmon2  22016  evlslem2  22034  evlslem3  22035  evlslem1  22037  evlsvvvallem2  22047  psdval  22102  rrxmet  25364  mdegldg  26027  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgamcvglem  27006  upgrres1lem1  29382  frgrwopreg1  30393  dlwwlknondlwlknonen  30441  nsgmgc  33493  nsgqusf1o  33497  ssdifidl  33538  extvfv  33698  extvfvcl  33701  extvfvalf  33702  issply  33719  esplyfval2  33723  esplympl  33725  esplyfv  33728  esplyfval3  33730  esplyind  33731  eulerpartlem1  34524  eulerpartlemt  34528  eulerpartgbij  34529  ballotlemoex  34643  satffunlem2lem2  35600  mapdunirnN  41910  mplmapghm  42807  selvvvval  42828  evlsmhpvvval  42838  pwfi2en  43339  smfresal  47032  oddiadd  48420  2zrngadd  48489  2zrngmul  48497