Theorem rabidim2 45553

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

Syntax hints:   → wi 4   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391

This theorem is referenced by:  infnsuprnmpt  45700  preimagelt  47148  preimalegt  47149  pimrecltpos  47157  pimiooltgt  47159  pimrecltneg  47173  smfaddlem1  47212  smflimlem2  47221  smfrec  47238  smfmullem4  47243  smfdiv  47246  smfsupxr  47265  smfinflem  47266  smflimsuplem7  47275  smflimsuplem8  47276  fsupdm  47291  finfdm  47295