Theorem rabexd 4846

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  {crab 2945  Vcvv 3231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-in 3614  df-ss 3621

This theorem is referenced by:  rabex2  4847  zorn2lem1  9356  sylow2a  18080  evlslem6  19561  mretopd  20944  cusgrexilem1  26391  vtxdgf  26423  stoweidlem35  40570  stoweidlem50  40585  stoweidlem57  40592  stoweidlem59  40594  subsaliuncllem  40893  subsaliuncl  40894  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302  smflimlem6  41305  smfrec  41317  smfpimcclem  41334  smfsuplem1  41338  smfinflem  41344  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem3  41349  smflimsuplem4  41350  smflimsuplem5  41351  smflimsuplem7  41353  fvmptrab  41631