Theorem rabex2 5291

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3402  Vcvv 3444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rab2ex  5292  mapfien2  9336  cantnffval  9592  nqex  10852  gsumvalx  18585  psgnfval  19414  odval  19448  sylow1lem2  19513  sylow3lem6  19546  ablfaclem1  20001  psrass1lem  21874  psrbas  21875  psrelbas  21876  psrmulfval  21885  psrmulcllem  21887  psrvscaval  21892  psr0cl  21894  psr0lid  21895  psrnegcl  21896  psrlinv  21897  psr1cl  21903  psrlidm  21904  psrdi  21907  psrdir  21908  psrass23l  21909  psrcom  21910  psrass23  21911  mvrval  21924  mplsubglem  21941  mpllsslem  21942  mplsubrglem  21946  mplvscaval  21958  mplmon  21975  mplmonmul  21976  mplcoe1  21977  ltbval  21983  mplmon2  22001  evlslem2  22019  evlslem3  22020  evlslem1  22022  psdval  22079  rrxmet  25341  mdegldg  26004  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgamcvglem  26983  upgrres1lem1  29289  frgrwopreg1  30297  dlwwlknondlwlknonen  30345  nsgmgc  33376  nsgqusf1o  33380  ssdifidl  33421  eulerpartlem1  34351  eulerpartlemt  34355  eulerpartgbij  34356  ballotlemoex  34470  satffunlem2lem2  35386  mapdunirnN  41637  mplmapghm  42537  evlsvvvallem2  42543  selvvvval  42566  evlsmhpvvval  42576  pwfi2en  43079  smfresal  46779  oddiadd  48155  2zrngadd  48224  2zrngmul  48232