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

Theorem rabexd 5127
 Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5128. (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 5125 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4syl5eqel 2887 1 (𝜑𝐵 ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1522   ∈ wcel 2081  {crab 3109  Vcvv 3437 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-sep 5094 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-in 3866  df-ss 3874 This theorem is referenced by:  rabex2  5128  zorn2lem1  9764  sylow2a  18474  evlslem6  19980  mhpaddcl  20021  mhpinvcl  20022  mhpvscacl  20024  mretopd  21384  cusgrexilem1  26904  vtxdgf  26936  tocycval  30397  stoweidlem35  41862  stoweidlem50  41877  stoweidlem57  41884  stoweidlem59  41886  subsaliuncllem  42182  subsaliuncl  42183  smflimlem1  42589  smflimlem2  42590  smflimlem3  42591  smflimlem6  42594  smfrec  42606  smfpimcclem  42623  smfsuplem1  42627  smfinflem  42633  smflimsuplem1  42636  smflimsuplem2  42637  smflimsuplem3  42638  smflimsuplem4  42639  smflimsuplem5  42640  smflimsuplem7  42642  fvmptrab  43007  prproropen  43152
 Copyright terms: Public domain W3C validator