| 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 3432 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 2 | 1 | simplbi 502 | 1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∈ wcel 2145 {crab 3412 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-12 2213 ax-ext 2732 |
| This proof depends on definitions: df-bi 210 df-an 402 df-tru 1573 df-ex 1813 df-sb 2100 df-clab 2739 df-cleq 2752 df-clel 2835 df-rab 3413 |
| This theorem is used by: frgrwopreglem5 30841 frgrwopreg 30843 rabexgfGS 33014 ssrab2f 46047 infnsuprnmpt 46177 preimagelt 47625 preimalegt 47626 pimrecltpos 47634 pimiooltgt 47636 pimrecltneg 47650 smfresal 47714 smfpimbor1lem2 47725 smflimmpt 47736 smfsupmpt 47741 smfinfmpt 47745 smflimsuplem7 47752 smflimsuplem8 47753 smflimsupmpt 47755 smfliminfmpt 47758 fsupdm 47768 finfdm 47772 |
| Copyright terms: Public domain | W3C validator |