Theorem rabex2 5346

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  {crab 3432  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979  df-pw 4606

This theorem is referenced by:  rab2ex  5347  mapfien2  9446  cantnffval  9700  nqex  10960  gsumvalx  18701  psgnfval  19532  odval  19566  sylow1lem2  19631  sylow3lem6  19664  ablfaclem1  20119  psrass1lem  21969  psrbas  21970  psrelbas  21971  psrmulfval  21980  psrmulcllem  21982  psrvscaval  21987  psr0cl  21989  psr0lid  21990  psrnegcl  21991  psrlinv  21992  psr1cl  21998  psrlidm  21999  psrdi  22002  psrdir  22003  psrass23l  22004  psrcom  22005  psrass23  22006  mvrval  22019  mplsubglem  22036  mpllsslem  22037  mplsubrglem  22041  mplvscaval  22053  mplmon  22070  mplmonmul  22071  mplcoe1  22072  ltbval  22078  mplmon2  22102  evlslem2  22120  evlslem3  22121  evlslem1  22123  psdval  22180  rrxmet  25455  mdegldg  26119  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvglem  27097  upgrres1lem1  29340  frgrwopreg1  30346  dlwwlknondlwlknonen  30394  nsgmgc  33419  nsgqusf1o  33423  ssdifidl  33464  eulerpartlem1  34348  eulerpartlemt  34352  eulerpartgbij  34353  ballotlemoex  34466  satffunlem2lem2  35390  mapdunirnN  41632  mplmapghm  42542  evlsvvvallem2  42548  selvvvval  42571  evlsmhpvvval  42581  pwfi2en  43085  smfresal  46743  oddiadd  48017  2zrngadd  48086  2zrngmul  48094