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

Theorem rabexd 5340
Description: Separation Scheme in terms of a restricted class abstraction, deduction form of rabex2 5341. (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 5337 . . 3 (𝐴𝑉 → {𝑥𝐴𝜓} ∈ V)
42, 3syl 17 . 2 (𝜑 → {𝑥𝐴𝜓} ∈ V)
51, 4eqeltrid 2845 1 (𝜑𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  {crab 3436  Vcvv 3480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-pw 4602
This theorem is referenced by:  rabex2  5341  zorn2lem1  10536  sylow2a  19637  psrascl  21999  evlslem6  22105  mhpaddcl  22155  mhmcompl  22384  mhmcoaddmpl  22385  mretopd  23100  cusgrexilem1  29456  vtxdgf  29489  mntoval  32972  tocycval  33128  prmidlval  33465  isprimroot  42094  primrootsunit1  42098  unitscyglem1  42196  evlsvvval  42573  evlsbagval  42576  mhpind  42604  stoweidlem35  46050  stoweidlem50  46065  stoweidlem57  46072  stoweidlem59  46074  subsaliuncllem  46372  subsaliuncl  46373  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  smflimlem6  46791  smfrec  46804  smfpimcclem  46822  smfsuplem1  46826  smfinflem  46832  smflimsuplem1  46835  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem4  46838  smflimsuplem5  46839  smflimsuplem7  46841  fvmptrab  47304  prproropen  47495  stgrvtx  47921  stgriedg  47922  gpgvtx  48002  gpgiedg  48003
  Copyright terms: Public domain W3C validator