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  9401  cantnffval  9664  nqex  11008  gsumvalx  18865  psgnfval  19714  odval  19748  sylow1lem2  19813  sylow3lem6  19846  ablfaclem1  20301  ssdifidl  21641  psrass1lem  22241  psrbas  22242  psrelbas  22243  psrmulfval  22251  psrmulcllem  22253  psrvscaval  22258  psr0cl  22260  psr0lid  22261  psrnegcl  22262  psrlinv  22263  psr1cl  22268  psrlidm  22269  psrdi  22272  psrdir  22273  psrass23l  22274  psrcom  22275  psrass23  22276  mvrval  22289  mplsubglem  22306  mpllsslem  22307  mplsubrglem  22311  mplvscaval  22323  mplmon  22344  mplmonmul  22345  mplcoe1  22346  ltbval  22352  mplmon2  22370  evlslem2  22388  evlslem3  22389  evlslem1  22391  evlsvvvallem2  22401  mplmapghm  22431  selvvvval  22451  psdval  22480  rrxmet  25729  mdegldg  26384  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgamcvglem  27367  angmgmlem  29395  angmgmbas  29398  upgrres1lem1  29890  frgrwopreg1  30919  dlwwlknondlwlknonen  30967  nsgmgc  33963  nsgqusf1o  33967  extvfv  34165  extvfvcl  34168  extvfvalf  34169  psrgsum  34180  psrmon  34181  psrmonmul  34182  psrmonmul2  34183  psrmonprod  34184  mplmonprod  34186  issply  34193  esplyfval2  34197  esplympl  34199  esplyfv  34202  esplyfval3  34204  esplyind  34207  eulerpartlem1  34999  eulerpartlemt  35003  eulerpartgbij  35004  ballotlemoex  35118  satffunlem2lem2  36171  mapdunirnN  42708  evlsmhpvvval  43624  pwfi2en  44099  smfresal  47798  oddiadd  49271  2zrngadd  49340  2zrngmul  49348