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 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  frgrwopreglem5  30922  frgrwopreg  30924  rabexgfGS  33095  ssrab2f  46132  infnsuprnmpt  46262  preimagelt  47709  preimalegt  47710  pimrecltpos  47718  pimiooltgt  47720  pimrecltneg  47734  smfresal  47798  smfpimbor1lem2  47809  smflimmpt  47820  smfsupmpt  47825  smfinfmpt  47829  smflimsuplem7  47836  smflimsuplem8  47837  smflimsupmpt  47839  smfliminfmpt  47842  fsupdm  47852  finfdm  47856