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

Theorem rabexd 4741
 Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4742. (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 4739 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4syl5eqel 2692 1 (𝜑𝐵 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-in 3547  df-ss 3554 This theorem is referenced by:  rabex2  4742  rabex2OLD  4744  zorn2lem1  9201  sylow2a  17857  evlslem6  19334  mretopd  20706  cusgraexilem1  25995  stoweidlem35  38928  stoweidlem50  38943  stoweidlem57  38950  stoweidlem59  38952  subsaliuncllem  39251  subsaliuncl  39252  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659  smflimlem6  39662  smfrec  39674  usgrexi  40661  vtxdgf  40686
 Copyright terms: Public domain W3C validator