![]() |
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 3451 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | 1 | simplbi 497 | 1 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 {crab 3431 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 |
This theorem is referenced by: frgrwopreglem5 29842 frgrwopreg 29844 rabexgfGS 32007 ssrab2f 44108 infnsuprnmpt 44253 preimagelt 45714 preimalegt 45715 pimrecltpos 45723 pimrecltneg 45739 smfresal 45803 smfpimbor1lem2 45814 smflimmpt 45825 smfsupmpt 45830 smfinfmpt 45834 smflimsuplem7 45841 smflimsuplem8 45842 smflimsupmpt 45844 smfliminfmpt 45847 fsupdm 45857 finfdm 45861 |
Copyright terms: Public domain | W3C validator |