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

Theorem rabidim1 3297
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 3295 . 2 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
21simplbi 492 1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  {crab 3091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-tru 1657  df-ex 1876  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-rab 3096
This theorem is referenced by:  frgrwopreglem5  27662  frgrwopreg  27664  ssrab2f  40046  infnsuprnmpt  40200  pimrecltpos  41653  pimrecltneg  41667  smfresal  41729  smfpimbor1lem2  41740  smflimmpt  41750  smfsupmpt  41755  smfinfmpt  41759  smflimsuplem7  41766  smflimsuplem8  41767  smflimsupmpt  41769  smfliminfmpt  41772
  Copyright terms: Public domain W3C validator