Theorem rabidim2 45042

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

Syntax hints:   → wi 4   ∈ wcel 2106  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434

This theorem is referenced by:  infnsuprnmpt  45195  preimagelt  46655  preimalegt  46656  pimrecltpos  46664  pimiooltgt  46666  pimrecltneg  46680  smfaddlem1  46719  smflimlem2  46728  smfrec  46745  smfmullem4  46750  smfdiv  46753  smfsupxr  46772  smfinflem  46773  smflimsuplem7  46782  smflimsuplem8  46783  fsupdm  46798  finfdm  46802