Theorem rabexd 5287

Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5288. (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 5284	. . 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 3401  Vcvv 3442

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 5243

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 3402  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  rabex2  5288  zorn2lem1  10418  sylow2a  19560  psrascl  21946  evlslem6  22048  evlsvvval  22060  mhpaddcl  22106  mhmcompl  22336  mhmcoaddmpl  22337  mretopd  23048  cusgrexilem1  29524  vtxdgf  29557  mntoval  33075  tocycval  33202  fxpval  33259  prmidlval  33530  extvfvcl  33713  isprimroot  42463  primrootsunit1  42467  unitscyglem1  42565  evlsbagval  42927  mhpind  42952  stoweidlem35  46393  stoweidlem50  46408  stoweidlem57  46415  stoweidlem59  46417  subsaliuncllem  46715  subsaliuncl  46716  smflimlem1  47129  smflimlem2  47130  smflimlem3  47131  smflimlem6  47134  smfrec  47147  smfpimcclem  47165  smfsuplem1  47169  smfinflem  47175  smflimsuplem1  47178  smflimsuplem2  47179  smflimsuplem3  47180  smflimsuplem4  47181  smflimsuplem5  47182  smflimsuplem7  47184  fvmptrab  47652  prproropen  47868  stgrvtx  48314  stgriedg  48315  gpgvtx  48403  gpgiedg  48404