Theorem rabexd 5278

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {crab 3390  Vcvv 3430

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 2709  ax-sep 5232

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-in 3897  df-ss 3907  df-pw 4544

This theorem is referenced by:  rabex2  5279  zorn2lem1  10412  sylow2a  19588  psrascl  21970  evlslem6  22072  evlsvvval  22084  mhpaddcl  22130  mhmcompl  22358  mhmcoaddmpl  22359  mretopd  23070  cusgrexilem1  29525  vtxdgf  29558  mntoval  33060  tocycval  33187  fxpval  33244  prmidlval  33515  extvfvcl  33698  isprimroot  42549  primrootsunit1  42553  unitscyglem1  42651  evlsbagval  43019  mhpind  43044  stoweidlem35  46484  stoweidlem50  46499  stoweidlem57  46506  stoweidlem59  46508  subsaliuncllem  46806  subsaliuncl  46807  smflimlem1  47220  smflimlem2  47221  smflimlem3  47222  smflimlem6  47225  smfrec  47238  smfpimcclem  47256  smfsuplem1  47260  smfinflem  47266  smflimsuplem1  47269  smflimsuplem2  47270  smflimsuplem3  47271  smflimsuplem4  47272  smflimsuplem5  47273  smflimsuplem7  47275  fvmptrab  47755  prproropen  47983  stgrvtx  48445  stgriedg  48446  gpgvtx  48534  gpgiedg  48535