Theorem rabexd 5340

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {crab 3436  Vcvv 3480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by:  rabex2  5341  zorn2lem1  10536  sylow2a  19637  psrascl  21999  evlslem6  22105  mhpaddcl  22155  mhmcompl  22384  mhmcoaddmpl  22385  mretopd  23100  cusgrexilem1  29456  vtxdgf  29489  mntoval  32972  tocycval  33128  prmidlval  33465  isprimroot  42094  primrootsunit1  42098  unitscyglem1  42196  evlsvvval  42573  evlsbagval  42576  mhpind  42604  stoweidlem35  46050  stoweidlem50  46065  stoweidlem57  46072  stoweidlem59  46074  subsaliuncllem  46372  subsaliuncl  46373  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  smflimlem6  46791  smfrec  46804  smfpimcclem  46822  smfsuplem1  46826  smfinflem  46832  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem4  46838  smflimsuplem5  46839  smflimsuplem7  46841  fvmptrab  47304  prproropen  47495  stgrvtx  47921  stgriedg  47922  gpgvtx  48002  gpgiedg  48003