Theorem rabexd 5281

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3389  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906  df-pw 4543

This theorem is referenced by:  rabex2  5282  zorn2lem1  10418  sylow2a  19594  psrascl  21957  evlslem6  22059  evlsvvval  22071  mhpaddcl  22117  mhmcompl  22345  mhmcoaddmpl  22346  mretopd  23057  cusgrexilem1  29508  vtxdgf  29540  mntoval  33042  tocycval  33169  fxpval  33226  prmidlval  33497  extvfvcl  33680  isprimroot  42532  primrootsunit1  42536  unitscyglem1  42634  evlsbagval  43002  mhpind  43027  stoweidlem35  46463  stoweidlem50  46478  stoweidlem57  46485  stoweidlem59  46487  subsaliuncllem  46785  subsaliuncl  46786  smflimlem1  47199  smflimlem2  47200  smflimlem3  47201  smflimlem6  47204  smfrec  47217  smfpimcclem  47235  smfsuplem1  47239  smfinflem  47245  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  fvmptrab  47740  prproropen  47968  stgrvtx  48430  stgriedg  48431  gpgvtx  48519  gpgiedg  48520