Theorem rabex2 5309

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {crab 3416  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-pw 4562

This theorem is used by:  rab2ex  5310  mapfien2  9438  cantnffval  9701  nqex  11047  gsumvalx  18915  psgnfval  19765  odval  19799  sylow1lem2  19864  sylow3lem6  19897  ablfaclem1  20352  ssdifidl  21692  psrass1lem  22296  psrbas  22297  psrelbas  22298  psrmulfval  22306  psrmulcllem  22308  psrvscaval  22313  psr0cl  22315  psr0lid  22316  psrnegcl  22317  psrlinv  22318  psr1cl  22323  psrlidm  22324  psrdi  22327  psrdir  22328  psrass23l  22329  psrcom  22330  psrass23  22331  mvrval  22344  mplsubglem  22361  mpllsslem  22362  mplsubrglem  22366  mplvscaval  22378  mplmon  22399  mplmonmul  22400  mplcoe1  22401  ltbval  22407  mplmon2  22425  evlslem2  22443  evlslem3  22444  evlslem1  22446  evlsvvvallem2  22456  mplmapghm  22486  selvvvval  22506  psdval  22535  rrxmet  25784  mdegldg  26439  lgamgulmlem5  27417  lgamgulmlem6  27418  lgamgulm2  27420  lgamcvglem  27424  angmgmlem  29452  angmgmbas  29455  upgrres1lem1  29947  frgrwopreg1  30976  dlwwlknondlwlknonen  31024  nsgmgc  34067  nsgqusf1o  34071  extvfv  34276  extvfvcl  34279  extvfvalf  34280  psrgsum  34291  psrmon  34292  psrmonmul  34293  psrmonmul2  34294  psrmonprod  34295  mplmonprod  34297  issply  34304  esplyfval2  34308  esplympl  34310  esplyfv  34313  esplyfval3  34315  esplyind  34318  eulerpartlem1  35110  eulerpartlemt  35114  eulerpartgbij  35115  ballotlemoex  35229  satffunlem2lem2  36379  mapdunirnN  42973  evlsmhpvvval  43889  pwfi2en  44365  smfresal  48071  oddiadd  49544  2zrngadd  49613  2zrngmul  49621