Theorem rabidim1 3425

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 3424	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
2	1	simplbi 497	1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109  {crab 3402

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  frgrwopreglem5  30300  frgrwopreg  30302  rabexgfGS  32478  ssrab2f  45104  infnsuprnmpt  45237  preimagelt  46690  preimalegt  46691  pimrecltpos  46699  pimrecltneg  46715  smfresal  46779  smfpimbor1lem2  46790  smflimmpt  46801  smfsupmpt  46806  smfinfmpt  46810  smflimsuplem7  46817  smflimsuplem8  46818  smflimsupmpt  46820  smfliminfmpt  46823  fsupdm  46833  finfdm  46837