Theorem rabidim1 3445

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

Syntax hints:   → wi 4   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  frgrwopreglem5  30613  frgrwopreg  30615  rabexgfGS  32786  ssrab2f  45761  infnsuprnmpt  45891  preimagelt  47339  preimalegt  47340  pimrecltpos  47348  pimiooltgt  47350  pimrecltneg  47364  smfresal  47428  smfpimbor1lem2  47439  smflimmpt  47450  smfsupmpt  47455  smfinfmpt  47459  smflimsuplem7  47466  smflimsuplem8  47467  smflimsupmpt  47469  smfliminfmpt  47472  fsupdm  47482  finfdm  47486