| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rabssab | Structured version Visualization version GIF version | ||
| Description: A restricted class is a subclass of the corresponding unrestricted class. (Contributed by Mario Carneiro, 23-Dec-2016.) |
| Ref | Expression |
|---|---|
| rabssab | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rab 3416 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
| 2 | simpr 489 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜑) | |
| 3 | 2 | ss2abi 4019 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ 𝜑} |
| 4 | 1, 3 | eqsstri 3982 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ {𝑥 ∣ 𝜑} |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ∧ wa 400 ∈ wcel 2142 {cab 2740 {crab 3415 ⊆ wss 3904 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-9 2152 ax-ext 2734 |
| This proof depends on definitions: df-bi 210 df-an 401 df-tru 1572 df-ex 1809 df-sb 2096 df-clab 2741 df-cleq 2754 df-rab 3416 df-ss 3921 |
| This theorem is used by: epse 5642 riotasbc 7387 cshwsexa 14868 toponsspwpw 23090 dmtopon 23091 aannenlem2 26503 aalioulem2 26507 ballotlemfmpn 34894 fineqvnttrclse 35545 rencldnfilem 43575 rmxyelqirr 43665 rababg 44328 |
| Copyright terms: Public domain | W3C validator |