Theorem rabex2 5321

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {crab 3419  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-in 3938  df-ss 3948  df-pw 4582

This theorem is referenced by:  rab2ex  5322  mapfien2  9431  cantnffval  9685  nqex  10945  gsumvalx  18658  psgnfval  19486  odval  19520  sylow1lem2  19585  sylow3lem6  19618  ablfaclem1  20073  psrass1lem  21906  psrbas  21907  psrelbas  21908  psrmulfval  21917  psrmulcllem  21919  psrvscaval  21924  psr0cl  21926  psr0lid  21927  psrnegcl  21928  psrlinv  21929  psr1cl  21935  psrlidm  21936  psrdi  21939  psrdir  21940  psrass23l  21941  psrcom  21942  psrass23  21943  mvrval  21956  mplsubglem  21973  mpllsslem  21974  mplsubrglem  21978  mplvscaval  21990  mplmon  22007  mplmonmul  22008  mplcoe1  22009  ltbval  22015  mplmon2  22033  evlslem2  22051  evlslem3  22052  evlslem1  22054  psdval  22111  rrxmet  25378  mdegldg  26041  lgamgulmlem5  27012  lgamgulmlem6  27013  lgamgulm2  27015  lgamcvglem  27019  upgrres1lem1  29254  frgrwopreg1  30265  dlwwlknondlwlknonen  30313  nsgmgc  33375  nsgqusf1o  33379  ssdifidl  33420  eulerpartlem1  34328  eulerpartlemt  34332  eulerpartgbij  34333  ballotlemoex  34447  satffunlem2lem2  35370  mapdunirnN  41611  mplmapghm  42529  evlsvvvallem2  42535  selvvvval  42558  evlsmhpvvval  42568  pwfi2en  43072  smfresal  46760  oddiadd  48048  2zrngadd  48117  2zrngmul  48125