Theorem rabex2 5305

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

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

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 2732  ax-sep 5251

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rab2ex  5306  mapfien2  9379  cantnffval  9642  nqex  10932  gsumvalx  18778  psgnfval  19627  odval  19661  sylow1lem2  19726  sylow3lem6  19759  ablfaclem1  20214  ssdifidl  21548  psrass1lem  22148  psrbas  22149  psrelbas  22150  psrmulfval  22158  psrmulcllem  22160  psrvscaval  22165  psr0cl  22167  psr0lid  22168  psrnegcl  22169  psrlinv  22170  psr1cl  22175  psrlidm  22176  psrdi  22179  psrdir  22180  psrass23l  22181  psrcom  22182  psrass23  22183  mvrval  22196  mplsubglem  22213  mpllsslem  22214  mplsubrglem  22218  mplvscaval  22230  mplmon  22251  mplmonmul  22252  mplcoe1  22253  ltbval  22259  mplmon2  22277  evlslem2  22295  evlslem3  22296  evlslem1  22298  evlsvvvallem2  22308  mplmapghm  22338  selvvvval  22358  psdval  22387  rrxmet  25636  mdegldg  26291  lgamgulmlem5  27269  lgamgulmlem6  27270  lgamgulm2  27272  lgamcvglem  27276  angmgmlem  29274  angmgmbas  29277  upgrres1lem1  29769  frgrwopreg1  30798  dlwwlknondlwlknonen  30846  nsgmgc  33841  nsgqusf1o  33845  extvfv  34043  extvfvcl  34046  extvfvalf  34047  psrgsum  34058  psrmon  34059  psrmonmul  34060  psrmonmul2  34061  psrmonprod  34062  mplmonprod  34064  issply  34071  esplyfval2  34075  esplympl  34077  esplyfv  34080  esplyfval3  34082  esplyind  34085  eulerpartlem1  34878  eulerpartlemt  34882  eulerpartgbij  34883  ballotlemoex  34997  satffunlem2lem2  35985  mapdunirnN  42523  evlsmhpvvval  43441  pwfi2en  43938  smfresal  47616  oddiadd  49089  2zrngadd  49158  2zrngmul  49166