Theorem rabidim2 45711

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

Syntax hints:   → wi 4   ∈ wcel 2149  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  infnsuprnmpt  45856  preimagelt  47304  preimalegt  47305  pimrecltpos  47313  pimiooltgt  47315  pimrecltneg  47329  sssmf  47343  smfaddlem1  47368  smflimlem2  47377  smfrec  47394  smfmullem4  47399  smfdiv  47402  smfsupxr  47421  smfinflem  47422  smflimsuplem7  47431  smflimsuplem8  47432  fsupdm  47447  finfdm  47451