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

Theorem rabidim1 3456
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 3455 . 2 (𝑥 ∈ {𝑥𝐴𝜑} ↔ (𝑥𝐴𝜑))
21simplbi 497 1 (𝑥 ∈ {𝑥𝐴𝜑} → 𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434
This theorem is referenced by:  frgrwopreglem5  30350  frgrwopreg  30352  rabexgfGS  32527  ssrab2f  45057  infnsuprnmpt  45195  preimagelt  46655  preimalegt  46656  pimrecltpos  46664  pimrecltneg  46680  smfresal  46744  smfpimbor1lem2  46755  smflimmpt  46766  smfsupmpt  46771  smfinfmpt  46775  smflimsuplem7  46782  smflimsuplem8  46783  smflimsupmpt  46785  smfliminfmpt  46788  fsupdm  46798  finfdm  46802
  Copyright terms: Public domain W3C validator