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

Theorem rabexd 5288
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5289. (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 5286 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4eqeltrid 2842 1 (𝜑𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wcel 2106  {crab 3405  Vcvv 3443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5254
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  rabex2  5289  zorn2lem1  10428  sylow2a  19392  evlslem6  21475  mhpaddcl  21525  mhpvscacl  21528  mretopd  22427  cusgrexilem1  28273  vtxdgf  28305  mntoval  31725  tocycval  31840  prmidlval  32088  evlsbagval  40699  mhpind  40707  stoweidlem35  44208  stoweidlem50  44223  stoweidlem57  44230  stoweidlem59  44232  subsaliuncllem  44530  subsaliuncl  44531  smflimlem1  44944  smflimlem2  44945  smflimlem3  44946  smflimlem6  44949  smfrec  44962  smfpimcclem  44980  smfsuplem1  44984  smfinflem  44990  smflimsuplem1  44993  smflimsuplem2  44994  smflimsuplem3  44995  smflimsuplem4  44996  smflimsuplem5  44997  smflimsuplem7  44999  fvmptrab  45456  prproropen  45632
  Copyright terms: Public domain W3C validator