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

Theorem rabexd 5295
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5296. (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 5293 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4eqeltrid 2842 1 (𝜑𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  {crab 3410  Vcvv 3448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  rabex2  5296  zorn2lem1  10439  sylow2a  19408  evlslem6  21507  mhpaddcl  21557  mhpvscacl  21560  mretopd  22459  cusgrexilem1  28429  vtxdgf  28461  mntoval  31884  tocycval  31999  prmidlval  32249  evlsbagval  40777  mhpind  40798  stoweidlem35  44350  stoweidlem50  44365  stoweidlem57  44372  stoweidlem59  44374  subsaliuncllem  44672  subsaliuncl  44673  smflimlem1  45086  smflimlem2  45087  smflimlem3  45088  smflimlem6  45091  smfrec  45104  smfpimcclem  45122  smfsuplem1  45126  smfinflem  45132  smflimsuplem1  45135  smflimsuplem2  45136  smflimsuplem3  45137  smflimsuplem4  45138  smflimsuplem5  45139  smflimsuplem7  45141  fvmptrab  45598  prproropen  45774
  Copyright terms: Public domain W3C validator