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

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 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  frgrwopreglem5  30801  frgrwopreg  30803  rabexgfGS  32974  ssrab2f  45949  infnsuprnmpt  46079  preimagelt  47527  preimalegt  47528  pimrecltpos  47536  pimiooltgt  47538  pimrecltneg  47552  smfresal  47616  smfpimbor1lem2  47627  smflimmpt  47638  smfsupmpt  47643  smfinfmpt  47647  smflimsuplem7  47654  smflimsuplem8  47655  smflimsupmpt  47657  smfliminfmpt  47660  fsupdm  47670  finfdm  47674