Theorem rabidim1 3423

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402

This theorem is referenced by:  frgrwopreglem5  30412  frgrwopreg  30414  rabexgfGS  32590  ssrab2f  45480  infnsuprnmpt  45612  preimagelt  47061  preimalegt  47062  pimrecltpos  47070  pimiooltgt  47072  pimrecltneg  47086  smfresal  47150  smfpimbor1lem2  47161  smflimmpt  47172  smfsupmpt  47177  smfinfmpt  47181  smflimsuplem7  47188  smflimsuplem8  47189  smflimsupmpt  47191  smfliminfmpt  47194  fsupdm  47204  finfdm  47208