Theorem rabidim1 3442

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

Syntax hints:   → wi 4   ∈ wcel 2107  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420

This theorem is referenced by:  frgrwopreglem5  30268  frgrwopreg  30270  rabexgfGS  32446  ssrab2f  45079  infnsuprnmpt  45214  preimagelt  46671  preimalegt  46672  pimrecltpos  46680  pimrecltneg  46696  smfresal  46760  smfpimbor1lem2  46771  smflimmpt  46782  smfsupmpt  46787  smfinfmpt  46791  smflimsuplem7  46798  smflimsuplem8  46799  smflimsupmpt  46801  smfliminfmpt  46804  fsupdm  46814  finfdm  46818