Theorem rabex2 5313

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {crab 3418  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-in 3913  df-ss 3923  df-pw 4566

This theorem is used by:  rab2ex  5314  mapfien2  9376  cantnffval  9639  nqex  10923  gsumvalx  18766  psgnfval  19614  odval  19648  sylow1lem2  19713  sylow3lem6  19746  ablfaclem1  20201  ssdifidl  21535  psrass1lem  22133  psrbas  22134  psrelbas  22135  psrmulfval  22143  psrmulcllem  22145  psrvscaval  22150  psr0cl  22152  psr0lid  22153  psrnegcl  22154  psrlinv  22155  psr1cl  22160  psrlidm  22161  psrdi  22164  psrdir  22165  psrass23l  22166  psrcom  22167  psrass23  22168  mvrval  22181  mplsubglem  22198  mpllsslem  22199  mplsubrglem  22203  mplvscaval  22215  mplmon  22236  mplmonmul  22237  mplcoe1  22238  ltbval  22244  mplmon2  22262  evlslem2  22280  evlslem3  22281  evlslem1  22283  evlsvvvallem2  22293  mplmapghm  22323  selvvvval  22343  psdval  22372  rrxmet  25618  mdegldg  26274  lgamgulmlem5  27248  lgamgulmlem6  27249  lgamgulm2  27251  lgamcvglem  27255  upgrres1lem1  29717  frgrwopreg1  30740  dlwwlknondlwlknonen  30788  nsgmgc  33785  nsgqusf1o  33789  extvfv  33987  extvfvcl  33990  extvfvalf  33991  psrgsum  34002  psrmon  34003  psrmonmul  34004  psrmonmul2  34005  psrmonprod  34006  mplmonprod  34008  issply  34015  esplyfval2  34019  esplympl  34021  esplyfv  34024  esplyfval3  34026  esplyind  34029  eulerpartlem1  34822  eulerpartlemt  34826  eulerpartgbij  34827  ballotlemoex  34941  satffunlem2lem2  35935  mapdunirnN  42482  evlsmhpvvval  43385  pwfi2en  43882  smfresal  47560  oddiadd  48996  2zrngadd  49065  2zrngmul  49073