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

Theorem rabidim1 3365
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 3363 . 2 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
21simplbi 501 1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  {crab 3130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-rab 3135
This theorem is referenced by:  frgrwopreglem5  28084  frgrwopreg  28086  rabexgfGS  30246  ssrab2f  41537  infnsuprnmpt  41676  preimagelt  43128  preimalegt  43129  pimrecltpos  43135  pimrecltneg  43149  smfresal  43211  smfpimbor1lem2  43222  smflimmpt  43232  smfsupmpt  43237  smfinfmpt  43241  smflimsuplem7  43248  smflimsuplem8  43249  smflimsupmpt  43251  smfliminfmpt  43254
  Copyright terms: Public domain W3C validator