Theorem rabidim2 45107

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

Syntax hints:   → wi 4   ∈ wcel 2108  {crab 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  infnsuprnmpt  45257  preimagelt  46714  preimalegt  46715  pimrecltpos  46723  pimiooltgt  46725  pimrecltneg  46739  smfaddlem1  46778  smflimlem2  46787  smfrec  46804  smfmullem4  46809  smfdiv  46812  smfsupxr  46831  smfinflem  46832  smflimsuplem7  46841  smflimsuplem8  46842  fsupdm  46857  finfdm  46861