Theorem rabex2 5240

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

Syntax hints:   = wceq 1536   ∈ wcel 2113  {crab 3145  Vcvv 3497

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-in 3946  df-ss 3955

This theorem is referenced by:  rab2ex  5241  mapfien2  8875  cantnffval  9129  nqex  10348  gsumvalx  17889  psgnfval  18631  odval  18665  sylow1lem2  18727  sylow3lem6  18760  ablfaclem1  19210  psrass1lem  20160  psrbas  20161  psrelbas  20162  psrmulfval  20168  psrmulcllem  20170  psrvscaval  20175  psr0cl  20177  psr0lid  20178  psrnegcl  20179  psrlinv  20180  psr1cl  20185  psrlidm  20186  psrdi  20189  psrdir  20190  psrass23l  20191  psrcom  20192  psrass23  20193  mvrval  20204  mplsubglem  20217  mpllsslem  20218  mplsubrglem  20222  mplvscaval  20231  mplmon  20247  mplmonmul  20248  mplcoe1  20249  ltbval  20255  opsrtoslem2  20268  mplmon2  20276  evlslem2  20295  evlslem3  20296  evlslem1  20298  rrxmet  24014  mdegldg  24663  lgamgulmlem5  25613  lgamgulmlem6  25614  lgamgulm2  25616  lgamcvglem  25620  upgrres1lem1  27094  frgrwopreg1  28100  dlwwlknondlwlknonen  28148  eulerpartlem1  31629  eulerpartlemt  31633  eulerpartgbij  31634  ballotlemoex  31747  satffunlem2lem2  32657  mapdunirnN  38790  pwfi2en  39703  smfresal  43070  oddiadd  44088  2zrngadd  44215  2zrngmul  44223