![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabidim1 | Structured version Visualization version GIF version |
Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
rabidim1 | ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabid 3450 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2104 {crab 3430 |
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 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-12 2169 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 |
This theorem is referenced by: frgrwopreglem5 29841 frgrwopreg 29843 rabexgfGS 32006 ssrab2f 44107 infnsuprnmpt 44252 preimagelt 45713 preimalegt 45714 pimrecltpos 45722 pimrecltneg 45738 smfresal 45802 smfpimbor1lem2 45813 smflimmpt 45824 smfsupmpt 45829 smfinfmpt 45833 smflimsuplem7 45840 smflimsuplem8 45841 smflimsupmpt 45843 smfliminfmpt 45846 fsupdm 45856 finfdm 45860 |
Copyright terms: Public domain | W3C validator |