Theorem rabexd 5346

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  {crab 3433  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-pw 4607

This theorem is referenced by:  rabex2  5347  zorn2lem1  10534  sylow2a  19652  psrascl  22017  evlslem6  22123  mhpaddcl  22173  mhmcompl  22400  mhmcoaddmpl  22401  mretopd  23116  cusgrexilem1  29471  vtxdgf  29504  mntoval  32957  tocycval  33111  prmidlval  33445  isprimroot  42075  primrootsunit1  42079  unitscyglem1  42177  evlsvvval  42550  evlsbagval  42553  mhpind  42581  stoweidlem35  45991  stoweidlem50  46006  stoweidlem57  46013  stoweidlem59  46015  subsaliuncllem  46313  subsaliuncl  46314  smflimlem1  46727  smflimlem2  46728  smflimlem3  46729  smflimlem6  46732  smfrec  46745  smfpimcclem  46763  smfsuplem1  46767  smfinflem  46773  smflimsuplem1  46776  smflimsuplem2  46777  smflimsuplem3  46778  smflimsuplem4  46779  smflimsuplem5  46780  smflimsuplem7  46782  fvmptrab  47242  prproropen  47433  stgrvtx  47857  stgriedg  47858  gpgvtx  47938  gpgiedg  47939