Theorem rabexd 4814

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4815. (Contributed by AV, 16-Jul-2019.)

Hypotheses

Ref	Expression
rabexd.1	|- B = { x e. A | ps }
rabexd.2	|- ( ph -> A e. V )

Assertion

Ref	Expression
rabexd	|- ( ph -> B e. _V )

Distinct variable group:   x, A

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

Proof of Theorem rabexd

Step	Hyp	Ref	Expression
1		rabexd.1	. 2 |- B = { x e. A | ps }
2		rabexd.2	. . 3 |- ( ph -> A e. V )
3		rabexg 4812	. . 3 |- ( A e. V -> { x e. A | ps } e. _V )
4	2, 3	syl 17	. 2 |- ( ph -> { x e. A | ps } e. _V )
5	1, 4	syl5eqel 2705	1 |- ( ph -> B e. _V )

Syntax hints:   -> wi 4   = 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:  rabex2  4815  rabex2OLD  4817  zorn2lem1  9318  sylow2a  18034  evlslem6  19513  mretopd  20896  cusgrexilem1  26335  vtxdgf  26367  stoweidlem35  40252  stoweidlem50  40267  stoweidlem57  40274  stoweidlem59  40276  subsaliuncllem  40575  subsaliuncl  40576  smflimlem1  40979  smflimlem2  40980  smflimlem3  40981  smflimlem6  40984  smfrec  40996  smfpimcclem  41013  smfsuplem1  41017  smfinflem  41023  smflimsuplem1  41026  smflimsuplem2  41027  smflimsuplem3  41028  smflimsuplem4  41029  smflimsuplem5  41030  smflimsuplem7  41032