Theorem rabexd 5301

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {crab 3413  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  rabex2  5302  zorn2lem1  10574  sylow2a  19833  prmidlval  21618  psrascl  22286  evlslem6  22390  evlsvvval  22402  mhmcompl  22430  mhmcoaddmpl  22432  mhpaddcl  22472  mretopd  23410  plngval  29255  angmgmval  29394  cusgrexilem1  30020  vtxdgf  30052  mntoval  33543  tocycval  33669  fxpval  33726  selvply1rhmlemb  34151  extvfvcl  34168  isprimroot  43143  primrootsunit1  43147  unitscyglem1  43245  evlsbagval  43614  mhpind  43622  stoweidlem35  47044  stoweidlem50  47059  stoweidlem57  47066  stoweidlem59  47068  subsaliuncllem  47366  subsaliuncl  47367  smflimlem1  47780  smflimlem2  47781  smflimlem3  47782  smflimlem6  47785  smfrec  47798  smfpimcclem  47816  smfsuplem1  47820  smfinflem  47826  smflimsuplem1  47829  smflimsuplem2  47830  smflimsuplem3  47831  smflimsuplem4  47832  smflimsuplem5  47833  smflimsuplem7  47835  fvmptrab  48361  prproropen  48589  stgrvtx  49051  stgriedg  49052  gpgvtx  49140  gpgiedg  49141