Theorem rabexd 5285

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {crab 3399  Vcvv 3440

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918  df-pw 4556

This theorem is referenced by:  rabex2  5286  zorn2lem1  10406  sylow2a  19548  psrascl  21934  evlslem6  22036  evlsvvval  22048  mhpaddcl  22094  mhmcompl  22324  mhmcoaddmpl  22325  mretopd  23036  cusgrexilem1  29512  vtxdgf  29545  mntoval  33064  tocycval  33190  fxpval  33247  prmidlval  33518  extvfvcl  33701  isprimroot  42347  primrootsunit1  42351  unitscyglem1  42449  evlsbagval  42812  mhpind  42837  stoweidlem35  46279  stoweidlem50  46294  stoweidlem57  46301  stoweidlem59  46303  subsaliuncllem  46601  subsaliuncl  46602  smflimlem1  47015  smflimlem2  47016  smflimlem3  47017  smflimlem6  47020  smfrec  47033  smfpimcclem  47051  smfsuplem1  47055  smfinflem  47061  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem3  47066  smflimsuplem4  47067  smflimsuplem5  47068  smflimsuplem7  47070  fvmptrab  47538  prproropen  47754  stgrvtx  48200  stgriedg  48201  gpgvtx  48289  gpgiedg  48290