Theorem rabexd 5348

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  {crab 3428  Vcvv 3472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700  ax-sep 5307

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-rab 3429  df-v 3474  df-in 3966  df-ss 3976  df-pw 4612

This theorem is referenced by:  rabex2  5349  zorn2lem1  10546  sylow2a  19639  psrascl  22010  evlslem6  22118  mhpaddcl  22167  mhpvscacl  22170  mhmcompl  22394  mhmcoaddmpl  22395  mretopd  23110  cusgrexilem1  29398  vtxdgf  29431  mntoval  32880  tocycval  33015  prmidlval  33343  isprimroot  41839  primrootsunit1  41843  unitscyglem1  41941  evlsvvval  42287  evlsbagval  42290  mhpind  42318  stoweidlem35  45726  stoweidlem50  45741  stoweidlem57  45748  stoweidlem59  45750  subsaliuncllem  46048  subsaliuncl  46049  smflimlem1  46462  smflimlem2  46463  smflimlem3  46464  smflimlem6  46467  smfrec  46480  smfpimcclem  46498  smfsuplem1  46502  smfinflem  46508  smflimsuplem1  46511  smflimsuplem2  46512  smflimsuplem3  46513  smflimsuplem4  46514  smflimsuplem5  46515  smflimsuplem7  46517  fvmptrab  46975  prproropen  47150