Theorem rabidim1 3433

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  frgrwopreglem5  30841  frgrwopreg  30843  rabexgfGS  33014  ssrab2f  46047  infnsuprnmpt  46177  preimagelt  47625  preimalegt  47626  pimrecltpos  47634  pimiooltgt  47636  pimrecltneg  47650  smfresal  47714  smfpimbor1lem2  47725  smflimmpt  47736  smfsupmpt  47741  smfinfmpt  47745  smflimsuplem7  47752  smflimsuplem8  47753  smflimsupmpt  47755  smfliminfmpt  47758  fsupdm  47768  finfdm  47772