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

Theorem rabidim1 3459
Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Assertion
Ref Expression
rabidim1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)

Proof of Theorem rabidim1
StepHypRef Expression
1 rabid 3458 . 2 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
21simplbi 497 1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  {crab 3436
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-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437
This theorem is referenced by:  frgrwopreglem5  30340  frgrwopreg  30342  rabexgfGS  32518  ssrab2f  45122  infnsuprnmpt  45257  preimagelt  46714  preimalegt  46715  pimrecltpos  46723  pimrecltneg  46739  smfresal  46803  smfpimbor1lem2  46814  smflimmpt  46825  smfsupmpt  46830  smfinfmpt  46834  smflimsuplem7  46841  smflimsuplem8  46842  smflimsupmpt  46844  smfliminfmpt  46847  fsupdm  46857  finfdm  46861
  Copyright terms: Public domain W3C validator