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 1570   ∈ wcel 2145  {crab 3413  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rab2ex  5303  mapfien2  9394  cantnffval  9657  nqex  11001  gsumvalx  18858  psgnfval  19707  odval  19741  sylow1lem2  19806  sylow3lem6  19839  ablfaclem1  20294  ssdifidl  21634  psrass1lem  22234  psrbas  22235  psrelbas  22236  psrmulfval  22244  psrmulcllem  22246  psrvscaval  22251  psr0cl  22253  psr0lid  22254  psrnegcl  22255  psrlinv  22256  psr1cl  22261  psrlidm  22262  psrdi  22265  psrdir  22266  psrass23l  22267  psrcom  22268  psrass23  22269  mvrval  22282  mplsubglem  22299  mpllsslem  22300  mplsubrglem  22304  mplvscaval  22316  mplmon  22337  mplmonmul  22338  mplcoe1  22339  ltbval  22345  mplmon2  22363  evlslem2  22381  evlslem3  22382  evlslem1  22384  evlsvvvallem2  22394  mplmapghm  22424  selvvvval  22444  psdval  22473  rrxmet  25722  mdegldg  26377  lgamgulmlem5  27353  lgamgulmlem6  27354  lgamgulm2  27356  lgamcvglem  27360  angmgmlem  29388  angmgmbas  29391  upgrres1lem1  29883  frgrwopreg1  30912  dlwwlknondlwlknonen  30960  nsgmgc  33956  nsgqusf1o  33960  extvfv  34158  extvfvcl  34161  extvfvalf  34162  psrgsum  34173  psrmon  34174  psrmonmul  34175  psrmonmul2  34176  psrmonprod  34177  mplmonprod  34179  issply  34186  esplyfval2  34190  esplympl  34192  esplyfv  34195  esplyfval3  34197  esplyind  34200  eulerpartlem1  34992  eulerpartlemt  34996  eulerpartgbij  34997  ballotlemoex  35111  satffunlem2lem2  36150  mapdunirnN  42687  evlsmhpvvval  43603  pwfi2en  44083  smfresal  47767  oddiadd  49240  2zrngadd  49309  2zrngmul  49317