MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabexd Structured version   Visualization version   GIF version

Theorem rabexd 5015
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5016. (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
StepHypRef Expression
1 rabexd.1 . 2 𝐵 = {𝑥𝐴𝜓}
2 rabexd.2 . . 3 (𝜑𝐴𝑉)
3 rabexg 5013 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4syl5eqel 2896 1 (𝜑𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2157  {crab 3107  Vcvv 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112  df-v 3400  df-in 3783  df-ss 3790
This theorem is referenced by:  rabex2  5016  zorn2lem1  9606  sylow2a  18238  evlslem6  19724  mretopd  21114  cusgrexilem1  26569  vtxdgf  26601  stoweidlem35  40732  stoweidlem50  40747  stoweidlem57  40754  stoweidlem59  40756  subsaliuncllem  41055  subsaliuncl  41056  smflimlem1  41462  smflimlem2  41463  smflimlem3  41464  smflimlem6  41467  smfrec  41479  smfpimcclem  41496  smfsuplem1  41500  smfinflem  41506  smflimsuplem1  41509  smflimsuplem2  41510  smflimsuplem3  41511  smflimsuplem4  41512  smflimsuplem5  41513  smflimsuplem7  41515  fvmptrab  41883
  Copyright terms: Public domain W3C validator