Theorem rabexd 5252

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {crab 3067  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rabex2  5253  zorn2lem1  10183  sylow2a  19139  evlslem6  21201  mhpaddcl  21251  mhpvscacl  21254  mretopd  22151  cusgrexilem1  27709  vtxdgf  27741  mntoval  31162  tocycval  31277  prmidlval  31514  evlsbagval  40198  mhpind  40206  stoweidlem35  43466  stoweidlem50  43481  stoweidlem57  43488  stoweidlem59  43490  subsaliuncllem  43786  subsaliuncl  43787  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  smflimlem6  44198  smfrec  44210  smfpimcclem  44227  smfsuplem1  44231  smfinflem  44237  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem3  44242  smflimsuplem4  44243  smflimsuplem5  44244  smflimsuplem7  44246  fvmptrab  44671  prproropen  44848