Theorem rabidim1 3419

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

Syntax hints:   → wi 4   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398

This theorem is referenced by:  frgrwopreglem5  30345  frgrwopreg  30347  rabexgfGS  32523  ssrab2f  45303  infnsuprnmpt  45436  preimagelt  46885  preimalegt  46886  pimrecltpos  46894  pimiooltgt  46896  pimrecltneg  46910  smfresal  46974  smfpimbor1lem2  46985  smflimmpt  46996  smfsupmpt  47001  smfinfmpt  47005  smflimsuplem7  47012  smflimsuplem8  47013  smflimsupmpt  47015  smfliminfmpt  47018  fsupdm  47028  finfdm  47032