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

Theorem rabexd 5200
 Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5201. (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 5198 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4eqeltrid 2894 1 (𝜑𝐵 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898 This theorem is referenced by:  rabex2  5201  zorn2lem1  9909  sylow2a  18739  evlslem6  20757  mhpaddcl  20806  mhpvscacl  20809  mretopd  21704  cusgrexilem1  27236  vtxdgf  27268  mntoval  30697  tocycval  30807  prmidlval  31027  stoweidlem35  42692  stoweidlem50  42707  stoweidlem57  42714  stoweidlem59  42716  subsaliuncllem  43012  subsaliuncl  43013  smflimlem1  43419  smflimlem2  43420  smflimlem3  43421  smflimlem6  43424  smfrec  43436  smfpimcclem  43453  smfsuplem1  43457  smfinflem  43463  smflimsuplem1  43466  smflimsuplem2  43467  smflimsuplem3  43468  smflimsuplem4  43469  smflimsuplem5  43470  smflimsuplem7  43472  fvmptrab  43863  prproropen  44040
 Copyright terms: Public domain W3C validator