Theorem rabidim2 46116

Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Assertion

Ref	Expression
rabidim2	⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑)

Proof of Theorem rabidim2

Step	Hyp	Ref	Expression
1		rabid 3433	. 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑))
2	1	simprbi 503	1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑)

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  infnsuprnmpt  46261  preimagelt  47708  preimalegt  47709  pimrecltpos  47717  pimiooltgt  47719  pimrecltneg  47733  sssmf  47747  smfaddlem1  47772  smflimlem2  47781  smfrec  47798  smfmullem4  47803  smfdiv  47806  smfsupxr  47825  smfinflem  47826  smflimsuplem7  47835  smflimsuplem8  47836  fsupdm  47851  finfdm  47855