Theorem rabexd 5127

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

Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  {crab 3109  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5094

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3866  df-ss 3874

This theorem is referenced by:  rabex2  5128  zorn2lem1  9764  sylow2a  18474  evlslem6  19980  mhpaddcl  20021  mhpinvcl  20022  mhpvscacl  20024  mretopd  21384  cusgrexilem1  26904  vtxdgf  26936  tocycval  30397  stoweidlem35  41862  stoweidlem50  41877  stoweidlem57  41884  stoweidlem59  41886  subsaliuncllem  42182  subsaliuncl  42183  smflimlem1  42589  smflimlem2  42590  smflimlem3  42591  smflimlem6  42594  smfrec  42606  smfpimcclem  42623  smfsuplem1  42627  smfinflem  42633  smflimsuplem1  42636  smflimsuplem2  42637  smflimsuplem3  42638  smflimsuplem4  42639  smflimsuplem5  42640  smflimsuplem7  42642  fvmptrab  43007  prproropen  43152