Theorem rabexd 5298

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3408  Vcvv 3450

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  rabex2  5299  zorn2lem1  10456  sylow2a  19556  psrascl  21895  evlslem6  21995  mhpaddcl  22045  mhmcompl  22274  mhmcoaddmpl  22275  mretopd  22986  cusgrexilem1  29373  vtxdgf  29406  mntoval  32915  tocycval  33072  fxpval  33129  prmidlval  33415  isprimroot  42088  primrootsunit1  42092  unitscyglem1  42190  evlsvvval  42558  evlsbagval  42561  mhpind  42589  stoweidlem35  46040  stoweidlem50  46055  stoweidlem57  46062  stoweidlem59  46064  subsaliuncllem  46362  subsaliuncl  46363  smflimlem1  46776  smflimlem2  46777  smflimlem3  46778  smflimlem6  46781  smfrec  46794  smfpimcclem  46812  smfsuplem1  46816  smfinflem  46822  smflimsuplem1  46825  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem4  46828  smflimsuplem5  46829  smflimsuplem7  46831  fvmptrab  47297  prproropen  47513  stgrvtx  47957  stgriedg  47958  gpgvtx  48038  gpgiedg  48039