Theorem rabidim1 3411

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  frgrwopreglem5  30391  frgrwopreg  30393  rabexgfGS  32569  ssrab2f  45547  infnsuprnmpt  45679  preimagelt  47127  preimalegt  47128  pimrecltpos  47136  pimiooltgt  47138  pimrecltneg  47152  smfresal  47216  smfpimbor1lem2  47227  smflimmpt  47238  smfsupmpt  47243  smfinfmpt  47247  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  fsupdm  47270  finfdm  47274