Theorem rabex2 4742

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  rab2ex  4743  mapfien2  8197  cantnffval  8443  nqex  9624  gsumvalx  17093  psgnfval  17743  odval  17776  sylow1lem2  17837  sylow3lem6  17870  ablfaclem1  18307  psrass1lem  19198  psrbas  19199  psrelbas  19200  psrmulfval  19206  psrmulcllem  19208  psrvscaval  19213  psr0cl  19215  psr0lid  19216  psrnegcl  19217  psrlinv  19218  psr1cl  19223  psrlidm  19224  psrdi  19227  psrdir  19228  psrass23l  19229  psrcom  19230  psrass23  19231  mvrval  19242  mplsubglem  19255  mpllsslem  19256  mplsubrglem  19260  mplvscaval  19269  mplmon  19284  mplmonmul  19285  mplcoe1  19286  ltbval  19292  opsrtoslem2  19306  mplmon2  19314  evlslem2  19333  evlslem3  19335  evlslem1  19336  rrxmet  22999  mdegldg  23630  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvglem  24566  eulerpartlem1  29756  eulerpartlemt  29760  eulerpartgbij  29761  ballotlemoex  29874  mapdunirnN  35957  pwfi2en  36685  smfresal  39673  upgrres1lem1  40528  frgrwopreg1  41487  oddiadd  41604  2zrngadd  41727  2zrngmul  41735