Theorem rabex2 4966

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

Syntax hints:   = wceq 1632   ∈ wcel 2139  {crab 3054  Vcvv 3340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-in 3722  df-ss 3729

This theorem is referenced by:  rab2ex  4967  mapfien2  8481  cantnffval  8735  nqex  9957  gsumvalx  17491  psgnfval  18140  odval  18173  sylow1lem2  18234  sylow3lem6  18267  ablfaclem1  18704  psrass1lem  19599  psrbas  19600  psrelbas  19601  psrmulfval  19607  psrmulcllem  19609  psrvscaval  19614  psr0cl  19616  psr0lid  19617  psrnegcl  19618  psrlinv  19619  psr1cl  19624  psrlidm  19625  psrdi  19628  psrdir  19629  psrass23l  19630  psrcom  19631  psrass23  19632  mvrval  19643  mplsubglem  19656  mpllsslem  19657  mplsubrglem  19661  mplvscaval  19670  mplmon  19685  mplmonmul  19686  mplcoe1  19687  ltbval  19693  opsrtoslem2  19707  mplmon2  19715  evlslem2  19734  evlslem3  19736  evlslem1  19737  rrxmet  23411  mdegldg  24045  lgamgulmlem5  24979  lgamgulmlem6  24980  lgamgulm2  24982  lgamcvglem  24986  upgrres1lem1  26421  frgrwopreg1  27493  dlwwlknondlwlknonen  27548  eulerpartlem1  30759  eulerpartlemt  30763  eulerpartgbij  30764  ballotlemoex  30877  mapdunirnN  37459  pwfi2en  38187  smfresal  41519  oddiadd  42342  2zrngadd  42465  2zrngmul  42473