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  19533  psrascl  21921  evlslem6  22021  mhpaddcl  22071  mhmcompl  22300  mhmcoaddmpl  22301  mretopd  23012  cusgrexilem1  29419  vtxdgf  29452  mntoval  32954  tocycval  33080  fxpval  33137  prmidlval  33401  isprimroot  42074  primrootsunit1  42078  unitscyglem1  42176  evlsvvval  42544  evlsbagval  42547  mhpind  42575  stoweidlem35  46026  stoweidlem50  46041  stoweidlem57  46048  stoweidlem59  46050  subsaliuncllem  46348  subsaliuncl  46349  smflimlem1  46762  smflimlem2  46763  smflimlem3  46764  smflimlem6  46767  smfrec  46780  smfpimcclem  46798  smfsuplem1  46802  smfinflem  46808  smflimsuplem1  46811  smflimsuplem2  46812  smflimsuplem3  46813  smflimsuplem4  46814  smflimsuplem5  46815  smflimsuplem7  46817  fvmptrab  47286  prproropen  47502  stgrvtx  47946  stgriedg  47947  gpgvtx  48027  gpgiedg  48028