Theorem rabidim1 3413

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

Syntax hints:   → wi 4   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392

This theorem is referenced by:  frgrwopreglem5  30410  frgrwopreg  30412  rabexgfGS  32588  ssrab2f  45572  infnsuprnmpt  45702  preimagelt  47150  preimalegt  47151  pimrecltpos  47159  pimiooltgt  47161  pimrecltneg  47175  smfresal  47239  smfpimbor1lem2  47250  smflimmpt  47261  smfsupmpt  47266  smfinfmpt  47270  smflimsuplem7  47277  smflimsuplem8  47278  smflimsupmpt  47280  smfliminfmpt  47283  fsupdm  47293  finfdm  47297