Theorem rabexd 5290

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5291. (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 5287	. . 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 3402  Vcvv 3444

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 5246

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 3403  df-v 3446  df-in 3918  df-ss 3928  df-pw 4561

This theorem is referenced by:  rabex2  5291  zorn2lem1  10425  sylow2a  19525  psrascl  21864  evlslem6  21964  mhpaddcl  22014  mhmcompl  22243  mhmcoaddmpl  22244  mretopd  22955  cusgrexilem1  29342  vtxdgf  29375  mntoval  32881  tocycval  33038  fxpval  33095  prmidlval  33381  isprimroot  42054  primrootsunit1  42058  unitscyglem1  42156  evlsvvval  42524  evlsbagval  42527  mhpind  42555  stoweidlem35  46006  stoweidlem50  46021  stoweidlem57  46028  stoweidlem59  46030  subsaliuncllem  46328  subsaliuncl  46329  smflimlem1  46742  smflimlem2  46743  smflimlem3  46744  smflimlem6  46747  smfrec  46760  smfpimcclem  46778  smfsuplem1  46782  smfinflem  46788  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem3  46793  smflimsuplem4  46794  smflimsuplem5  46795  smflimsuplem7  46797  fvmptrab  47266  prproropen  47482  stgrvtx  47926  stgriedg  47927  gpgvtx  48007  gpgiedg  48008