Theorem rabexd 5236

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  {crab 3142  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  rabex2  5237  zorn2lem1  9918  sylow2a  18744  evlslem6  20294  mhpaddcl  20338  mhpinvcl  20339  mhpvscacl  20341  mretopd  21700  cusgrexilem1  27221  vtxdgf  27253  tocycval  30750  prmidlval  30954  stoweidlem35  42340  stoweidlem50  42355  stoweidlem57  42362  stoweidlem59  42364  subsaliuncllem  42660  subsaliuncl  42661  smflimlem1  43067  smflimlem2  43068  smflimlem3  43069  smflimlem6  43072  smfrec  43084  smfpimcclem  43101  smfsuplem1  43105  smfinflem  43111  smflimsuplem1  43114  smflimsuplem2  43115  smflimsuplem3  43116  smflimsuplem4  43117  smflimsuplem5  43118  smflimsuplem7  43120  fvmptrab  43511  prproropen  43690