Theorem rabidim1 3437

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

Syntax hints:   → wi 4   ∈ wcel 2143  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416

This theorem is referenced by:  frgrwopreglem5  30524  frgrwopreg  30526  rabexgfGS  32699  ssrab2f  45696  infnsuprnmpt  45826  preimagelt  47274  preimalegt  47275  pimrecltpos  47283  pimiooltgt  47285  pimrecltneg  47299  smfresal  47363  smfpimbor1lem2  47374  smflimmpt  47385  smfsupmpt  47390  smfinfmpt  47394  smflimsuplem7  47401  smflimsuplem8  47402  smflimsupmpt  47404  smfliminfmpt  47407  fsupdm  47417  finfdm  47421