Theorem rabidim2 45680

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

Syntax hints:   → wi 4   ∈ wcel 2142  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is referenced by:  infnsuprnmpt  45825  preimagelt  47273  preimalegt  47274  pimrecltpos  47282  pimiooltgt  47284  pimrecltneg  47298  sssmf  47312  smfaddlem1  47337  smflimlem2  47346  smfrec  47363  smfmullem4  47368  smfdiv  47371  smfsupxr  47390  smfinflem  47391  smflimsuplem7  47400  smflimsuplem8  47401  fsupdm  47416  finfdm  47420