Theorem rabexd 5257

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5258. (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 5255	. . 3 ⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
4	2, 3	syl 17	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} ∈ V)
5	1, 4	eqeltrid 2843	1 ⊢ (𝜑 → 𝐵 ∈ V)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  {crab 3068  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  rabex2  5258  zorn2lem1  10252  sylow2a  19224  evlslem6  21291  mhpaddcl  21341  mhpvscacl  21344  mretopd  22243  cusgrexilem1  27806  vtxdgf  27838  mntoval  31260  tocycval  31375  prmidlval  31612  evlsbagval  40275  mhpind  40283  stoweidlem35  43576  stoweidlem50  43591  stoweidlem57  43598  stoweidlem59  43600  subsaliuncllem  43896  subsaliuncl  43897  smflimlem1  44306  smflimlem2  44307  smflimlem3  44308  smflimlem6  44311  smfrec  44323  smfpimcclem  44340  smfsuplem1  44344  smfinflem  44350  smflimsuplem1  44353  smflimsuplem2  44354  smflimsuplem3  44355  smflimsuplem4  44356  smflimsuplem5  44357  smflimsuplem7  44359  fvmptrab  44784  prproropen  44960