Theorem rabexd 5279

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {crab 3394  Vcvv 3436

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 2701  ax-sep 5235

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-in 3910  df-ss 3920  df-pw 4553

This theorem is referenced by:  rabex2  5280  zorn2lem1  10390  sylow2a  19498  psrascl  21886  evlslem6  21986  mhpaddcl  22036  mhmcompl  22265  mhmcoaddmpl  22266  mretopd  22977  cusgrexilem1  29384  vtxdgf  29417  mntoval  32924  tocycval  33050  fxpval  33107  prmidlval  33374  isprimroot  42066  primrootsunit1  42070  unitscyglem1  42168  evlsvvval  42536  evlsbagval  42539  mhpind  42567  stoweidlem35  46016  stoweidlem50  46031  stoweidlem57  46038  stoweidlem59  46040  subsaliuncllem  46338  subsaliuncl  46339  smflimlem1  46752  smflimlem2  46753  smflimlem3  46754  smflimlem6  46757  smfrec  46770  smfpimcclem  46788  smfsuplem1  46792  smfinflem  46798  smflimsuplem1  46801  smflimsuplem2  46802  smflimsuplem3  46803  smflimsuplem4  46804  smflimsuplem5  46805  smflimsuplem7  46807  fvmptrab  47276  prproropen  47492  stgrvtx  47938  stgriedg  47939  gpgvtx  48027  gpgiedg  48028