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

Theorem rabexd 4846
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 4847. (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 4844 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4syl5eqel 2734 1 (𝜑𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030  {crab 2945  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-in 3614  df-ss 3621
This theorem is referenced by:  rabex2  4847  zorn2lem1  9356  sylow2a  18080  evlslem6  19561  mretopd  20944  cusgrexilem1  26391  vtxdgf  26423  stoweidlem35  40570  stoweidlem50  40585  stoweidlem57  40592  stoweidlem59  40594  subsaliuncllem  40893  subsaliuncl  40894  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302  smflimlem6  41305  smfrec  41317  smfpimcclem  41334  smfsuplem1  41338  smfinflem  41344  smflimsuplem1  41347  smflimsuplem2  41348  smflimsuplem3  41349  smflimsuplem4  41350  smflimsuplem5  41351  smflimsuplem7  41353  fvmptrab  41631
  Copyright terms: Public domain W3C validator