Theorem rabex2 4815

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	|- B = { x e. A | ps }
rabex2.2	|- A e. _V

Assertion

Ref	Expression
rabex2	|- B e. _V

Distinct variable group:   x, A

Allowed substitution hints:   ps( x)   B( x)

Proof of Theorem rabex2

Step	Hyp	Ref	Expression
1		rabex2.2	. 2 |- A e. _V
2		rabex2.1	. . 3 |- B = { x e. A | ps }
3		id 22	. . 3 |- ( A e. _V -> A e. _V )
4	2, 3	rabexd 4814	. 2 |- ( A e. _V -> B e. _V )
5	1, 4	ax-mp 5	1 |- B e. _V

Syntax hints:   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  rab2ex  4816  mapfien2  8314  cantnffval  8560  nqex  9745  gsumvalx  17270  psgnfval  17920  odval  17953  sylow1lem2  18014  sylow3lem6  18047  ablfaclem1  18484  psrass1lem  19377  psrbas  19378  psrelbas  19379  psrmulfval  19385  psrmulcllem  19387  psrvscaval  19392  psr0cl  19394  psr0lid  19395  psrnegcl  19396  psrlinv  19397  psr1cl  19402  psrlidm  19403  psrdi  19406  psrdir  19407  psrass23l  19408  psrcom  19409  psrass23  19410  mvrval  19421  mplsubglem  19434  mpllsslem  19435  mplsubrglem  19439  mplvscaval  19448  mplmon  19463  mplmonmul  19464  mplcoe1  19465  ltbval  19471  opsrtoslem2  19485  mplmon2  19493  evlslem2  19512  evlslem3  19514  evlslem1  19515  rrxmet  23191  mdegldg  23826  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgamcvglem  24766  upgrres1lem1  26201  frgrwopreg1  27182  eulerpartlem1  30429  eulerpartlemt  30433  eulerpartgbij  30434  ballotlemoex  30547  mapdunirnN  36939  pwfi2en  37667  smfresal  40995  oddiadd  41814  2zrngadd  41937  2zrngmul  41945