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

Theorem rabidim1 3451
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 3450 . 2 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
21simplbi 496 1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2104  {crab 3430
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431
This theorem is referenced by:  frgrwopreglem5  29841  frgrwopreg  29843  rabexgfGS  32006  ssrab2f  44107  infnsuprnmpt  44252  preimagelt  45713  preimalegt  45714  pimrecltpos  45722  pimrecltneg  45738  smfresal  45802  smfpimbor1lem2  45813  smflimmpt  45824  smfsupmpt  45829  smfinfmpt  45833  smflimsuplem7  45840  smflimsuplem8  45841  smflimsupmpt  45843  smfliminfmpt  45846  fsupdm  45856  finfdm  45860
  Copyright terms: Public domain W3C validator