Theorem rabidim1 3436

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

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

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 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is used by:  frgrwopreglem5  30787  frgrwopreg  30789  rabexgfGS  32960  ssrab2f  45936  infnsuprnmpt  46066  preimagelt  47514  preimalegt  47515  pimrecltpos  47523  pimiooltgt  47525  pimrecltneg  47539  smfresal  47603  smfpimbor1lem2  47614  smflimmpt  47625  smfsupmpt  47630  smfinfmpt  47634  smflimsuplem7  47641  smflimsuplem8  47642  smflimsupmpt  47644  smfliminfmpt  47647  fsupdm  47657  finfdm  47661