Theorem rabexd 5310

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {crab 3415  Vcvv 3459

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 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  rabex2  5311  zorn2lem1  10510  sylow2a  19600  psrascl  21939  evlslem6  22039  mhpaddcl  22089  mhmcompl  22318  mhmcoaddmpl  22319  mretopd  23030  cusgrexilem1  29418  vtxdgf  29451  mntoval  32962  tocycval  33119  prmidlval  33452  isprimroot  42106  primrootsunit1  42110  unitscyglem1  42208  evlsvvval  42586  evlsbagval  42589  mhpind  42617  stoweidlem35  46064  stoweidlem50  46079  stoweidlem57  46086  stoweidlem59  46088  subsaliuncllem  46386  subsaliuncl  46387  smflimlem1  46800  smflimlem2  46801  smflimlem3  46802  smflimlem6  46805  smfrec  46818  smfpimcclem  46836  smfsuplem1  46840  smfinflem  46846  smflimsuplem1  46849  smflimsuplem2  46850  smflimsuplem3  46851  smflimsuplem4  46852  smflimsuplem5  46853  smflimsuplem7  46855  fvmptrab  47321  prproropen  47522  stgrvtx  47966  stgriedg  47967  gpgvtx  48047  gpgiedg  48048