Theorem rabexd 5358

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {crab 3443  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993  df-pw 4624

This theorem is referenced by:  rabex2  5359  zorn2lem1  10565  sylow2a  19661  psrascl  22022  evlslem6  22128  mhpaddcl  22178  mhmcompl  22405  mhmcoaddmpl  22406  mretopd  23121  cusgrexilem1  29474  vtxdgf  29507  mntoval  32955  tocycval  33101  prmidlval  33430  isprimroot  42050  primrootsunit1  42054  unitscyglem1  42152  evlsvvval  42518  evlsbagval  42521  mhpind  42549  stoweidlem35  45956  stoweidlem50  45971  stoweidlem57  45978  stoweidlem59  45980  subsaliuncllem  46278  subsaliuncl  46279  smflimlem1  46692  smflimlem2  46693  smflimlem3  46694  smflimlem6  46697  smfrec  46710  smfpimcclem  46728  smfsuplem1  46732  smfinflem  46738  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem4  46744  smflimsuplem5  46745  smflimsuplem7  46747  fvmptrab  47207  prproropen  47382