| 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 30801 frgrwopreg 30803 rabexgfGS 32974 ssrab2f 45949 infnsuprnmpt 46079 preimagelt 47527 preimalegt 47528 pimrecltpos 47536 pimiooltgt 47538 pimrecltneg 47552 smfresal 47616 smfpimbor1lem2 47627 smflimmpt 47638 smfsupmpt 47643 smfinfmpt 47647 smflimsuplem7 47654 smflimsuplem8 47655 smflimsupmpt 47657 smfliminfmpt 47660 fsupdm 47670 finfdm 47674 |
| Copyright terms: Public domain | W3C validator |