Theorem rabexd 5301

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {crab 3412  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-pw 4558

This theorem is used by:  rabex2  5302  zorn2lem1  10581  sylow2a  19842  prmidlval  21627  psrascl  22295  evlslem6  22399  evlsvvval  22411  mhmcompl  22439  mhmcoaddmpl  22441  mhpaddcl  22481  mretopd  23419  plngval  29264  angmgmval  29403  cusgrexilem1  30029  vtxdgf  30061  mntoval  33593  tocycval  33719  fxpval  33776  selvply1rhmlemb  34201  extvfvcl  34218  isprimroot  43280  primrootsunit1  43284  unitscyglem1  43382  evlsbagval  43751  mhpind  43759  stoweidlem35  47181  stoweidlem50  47196  stoweidlem57  47203  stoweidlem59  47205  subsaliuncllem  47503  subsaliuncl  47504  smflimlem1  47917  smflimlem2  47918  smflimlem3  47919  smflimlem6  47922  smfrec  47935  smfpimcclem  47953  smfsuplem1  47957  smfinflem  47963  smflimsuplem1  47966  smflimsuplem2  47967  smflimsuplem3  47968  smflimsuplem4  47969  smflimsuplem5  47970  smflimsuplem7  47972  fvmptrab  48498  prproropen  48726  stgrvtx  49188  stgriedg  49189  gpgvtx  49277  gpgiedg  49278