![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > rabidim2 | Structured version Visualization version GIF version |
Description: Membership in a restricted abstraction, implication. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
rabidim2 | ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabid 3451 | . 2 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | 1 | simprbi 496 | 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: infnsuprnmpt 44254 preimagelt 45715 preimalegt 45716 pimrecltpos 45724 pimiooltgt 45726 pimrecltneg 45740 smfaddlem1 45779 smflimlem2 45788 smfrec 45805 smfmullem4 45810 smfdiv 45813 smfsupxr 45832 smfinflem 45833 smflimsuplem7 45842 smflimsuplem8 45843 fsupdm 45858 finfdm 45862 |
Copyright terms: Public domain | W3C validator |