Theorem rabexd 5227

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

Syntax hints:   → wi 4   = wceq 1531   ∈ wcel 2108  {crab 3140  Vcvv 3493

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 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-in 3941  df-ss 3950

This theorem is referenced by:  rabex2  5228  zorn2lem1  9910  sylow2a  18736  evlslem6  20286  mhpaddcl  20330  mhpinvcl  20331  mhpvscacl  20333  mretopd  21692  cusgrexilem1  27213  vtxdgf  27245  tocycval  30743  prmidlval  30947  stoweidlem35  42311  stoweidlem50  42326  stoweidlem57  42333  stoweidlem59  42335  subsaliuncllem  42631  subsaliuncl  42632  smflimlem1  43038  smflimlem2  43039  smflimlem3  43040  smflimlem6  43043  smfrec  43055  smfpimcclem  43072  smfsuplem1  43076  smfinflem  43082  smflimsuplem1  43085  smflimsuplem2  43086  smflimsuplem3  43087  smflimsuplem4  43088  smflimsuplem5  43089  smflimsuplem7  43091  fvmptrab  43482  prproropen  43661