Theorem rabex2 5279

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3390  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rab2ex  5280  mapfien2  9316  cantnffval  9578  nqex  10840  gsumvalx  18638  psgnfval  19469  odval  19503  sylow1lem2  19568  sylow3lem6  19601  ablfaclem1  20056  psrass1lem  21925  psrbas  21926  psrelbas  21927  psrmulfval  21935  psrmulcllem  21937  psrvscaval  21942  psr0cl  21944  psr0lid  21945  psrnegcl  21946  psrlinv  21947  psr1cl  21952  psrlidm  21953  psrdi  21956  psrdir  21957  psrass23l  21958  psrcom  21959  psrass23  21960  mvrval  21973  mplsubglem  21990  mpllsslem  21991  mplsubrglem  21995  mplvscaval  22007  mplmon  22026  mplmonmul  22027  mplcoe1  22028  ltbval  22034  mplmon2  22052  evlslem2  22070  evlslem3  22071  evlslem1  22073  evlsvvvallem2  22083  psdval  22138  rrxmet  25388  mdegldg  26044  lgamgulmlem5  27013  lgamgulmlem6  27014  lgamgulm2  27016  lgamcvglem  27020  upgrres1lem1  29395  frgrwopreg1  30406  dlwwlknondlwlknonen  30454  nsgmgc  33490  nsgqusf1o  33494  ssdifidl  33535  extvfv  33695  extvfvcl  33698  extvfvalf  33699  psrgsum  33710  psrmon  33711  psrmonmul  33712  psrmonmul2  33713  psrmonprod  33714  mplmonprod  33716  issply  33723  esplyfval2  33727  esplympl  33729  esplyfv  33732  esplyfval3  33734  esplyind  33737  eulerpartlem1  34530  eulerpartlemt  34534  eulerpartgbij  34535  ballotlemoex  34649  satffunlem2lem2  35607  mapdunirnN  42113  mplmapghm  43014  selvvvval  43035  evlsmhpvvval  43045  pwfi2en  43546  smfresal  47237  oddiadd  48665  2zrngadd  48734  2zrngmul  48742