Theorem rabexd 5276

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {crab 3395  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-pw 4549

This theorem is referenced by:  rabex2  5277  zorn2lem1  10387  sylow2a  19531  psrascl  21916  evlslem6  22016  mhpaddcl  22066  mhmcompl  22295  mhmcoaddmpl  22296  mretopd  23007  cusgrexilem1  29417  vtxdgf  29450  mntoval  32963  tocycval  33077  fxpval  33134  prmidlval  33402  isprimroot  42185  primrootsunit1  42189  unitscyglem1  42287  evlsvvval  42655  evlsbagval  42658  mhpind  42686  stoweidlem35  46132  stoweidlem50  46147  stoweidlem57  46154  stoweidlem59  46156  subsaliuncllem  46454  subsaliuncl  46455  smflimlem1  46868  smflimlem2  46869  smflimlem3  46870  smflimlem6  46873  smfrec  46886  smfpimcclem  46904  smfsuplem1  46908  smfinflem  46914  smflimsuplem1  46917  smflimsuplem2  46918  smflimsuplem3  46919  smflimsuplem4  46920  smflimsuplem5  46921  smflimsuplem7  46923  fvmptrab  47391  prproropen  47607  stgrvtx  48053  stgriedg  48054  gpgvtx  48142  gpgiedg  48143