Theorem rabex2 5302

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  {crab 3412  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558

This theorem is used by:  rab2ex  5303  mapfien2  9408  cantnffval  9671  nqex  11015  gsumvalx  18874  psgnfval  19723  odval  19757  sylow1lem2  19822  sylow3lem6  19855  ablfaclem1  20310  ssdifidl  21650  psrass1lem  22250  psrbas  22251  psrelbas  22252  psrmulfval  22260  psrmulcllem  22262  psrvscaval  22267  psr0cl  22269  psr0lid  22270  psrnegcl  22271  psrlinv  22272  psr1cl  22277  psrlidm  22278  psrdi  22281  psrdir  22282  psrass23l  22283  psrcom  22284  psrass23  22285  mvrval  22298  mplsubglem  22315  mpllsslem  22316  mplsubrglem  22320  mplvscaval  22332  mplmon  22353  mplmonmul  22354  mplcoe1  22355  ltbval  22361  mplmon2  22379  evlslem2  22397  evlslem3  22398  evlslem1  22400  evlsvvvallem2  22410  mplmapghm  22440  selvvvval  22460  psdval  22489  rrxmet  25738  mdegldg  26393  lgamgulmlem5  27369  lgamgulmlem6  27370  lgamgulm2  27372  lgamcvglem  27376  angmgmlem  29404  angmgmbas  29407  upgrres1lem1  29899  frgrwopreg1  30928  dlwwlknondlwlknonen  30976  nsgmgc  34013  nsgqusf1o  34017  extvfv  34215  extvfvcl  34218  extvfvalf  34219  psrgsum  34230  psrmon  34231  psrmonmul  34232  psrmonmul2  34233  psrmonprod  34234  mplmonprod  34236  issply  34243  esplyfval2  34247  esplympl  34249  esplyfv  34252  esplyfval3  34254  esplyind  34257  eulerpartlem1  35049  eulerpartlemt  35053  eulerpartgbij  35054  ballotlemoex  35168  satffunlem2lem2  36261  mapdunirnN  42816  evlsmhpvvval  43732  pwfi2en  44208  smfresal  47906  oddiadd  49379  2zrngadd  49448  2zrngmul  49456