Theorem rabexd 5300

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {crab 3412  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3903  df-ss 3914  df-pw 4558

This theorem is used by:  rabex2  5301  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  43144  primrootsunit1  43148  unitscyglem1  43246  evlsbagval  43615  mhpind  43623  stoweidlem35  47045  stoweidlem50  47060  stoweidlem57  47067  stoweidlem59  47069  subsaliuncllem  47367  subsaliuncl  47368  smflimlem1  47781  smflimlem2  47782  smflimlem3  47783  smflimlem6  47786  smfrec  47799  smfpimcclem  47817  smfsuplem1  47821  smfinflem  47827  smflimsuplem1  47830  smflimsuplem2  47831  smflimsuplem3  47832  smflimsuplem4  47833  smflimsuplem5  47834  smflimsuplem7  47836  fvmptrab  48362  prproropen  48590  stgrvtx  49052  stgriedg  49053  gpgvtx  49141  gpgiedg  49142