Theorem rabexd 5295

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

Hypotheses

Ref	Expression
rabexd.1	⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
rabexd.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
rabexd	⊢ (𝜑 → 𝐵 ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem rabexd

Step	Hyp	Ref	Expression
1		rabexd.1	. 2 ⊢ 𝐵 = {𝑥 ∈ 𝐴 ∣ 𝜓}
2		rabexd.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		rabexg 5293	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
5	1, 4	eqeltrid 2836	1 ⊢ (𝜑 → 𝐵 ∈ V)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  {crab 3405  Vcvv 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  rabex2  5296  zorn2lem1  10441  sylow2a  19415  evlslem6  21528  mhpaddcl  21578  mhpvscacl  21581  mretopd  22480  cusgrexilem1  28450  vtxdgf  28482  mntoval  31912  tocycval  32027  prmidlval  32285  evlsbagval  40806  mhpind  40827  stoweidlem35  44396  stoweidlem50  44411  stoweidlem57  44418  stoweidlem59  44420  subsaliuncllem  44718  subsaliuncl  44719  smflimlem1  45132  smflimlem2  45133  smflimlem3  45134  smflimlem6  45137  smfrec  45150  smfpimcclem  45168  smfsuplem1  45172  smfinflem  45178  smflimsuplem1  45181  smflimsuplem2  45182  smflimsuplem3  45183  smflimsuplem4  45184  smflimsuplem5  45185  smflimsuplem7  45187  fvmptrab  45644  prproropen  45820