Theorem rabidim1 3333

Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Assertion

Ref	Expression
rabidim1	⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)

Proof of Theorem rabidim1

Step	Hyp	Ref	Expression
1		rabid 3331	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
2	1	simplbi 501	1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2111  {crab 3110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  frgrwopreglem5  28106  frgrwopreg  28108  rabexgfGS  30269  ssrab2f  41752  infnsuprnmpt  41888  preimagelt  43337  preimalegt  43338  pimrecltpos  43344  pimrecltneg  43358  smfresal  43420  smfpimbor1lem2  43431  smflimmpt  43441  smfsupmpt  43446  smfinfmpt  43450  smflimsuplem7  43457  smflimsuplem8  43458  smflimsupmpt  43460  smfliminfmpt  43463