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 3376 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | 1 | simplbi 498 | 1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 {crab 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-tru 1531 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-rab 3144 |
This theorem is referenced by: frgrwopreglem5 28027 frgrwopreg 28029 rabexgfGS 30189 ssrab2f 41260 infnsuprnmpt 41398 preimagelt 42857 preimalegt 42858 pimrecltpos 42864 pimrecltneg 42878 smfresal 42940 smfpimbor1lem2 42951 smflimmpt 42961 smfsupmpt 42966 smfinfmpt 42970 smflimsuplem7 42977 smflimsuplem8 42978 smflimsupmpt 42980 smfliminfmpt 42983 |
Copyright terms: Public domain | W3C validator |