| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > elpw | GIF version | ||
| Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 31-Dec-1993.) |
| Ref | Expression |
|---|---|
| elpw.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| elpw | ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elpw.1 | . 2 ⊢ 𝐴 ∈ V | |
| 2 | sseq1 3263 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
| 3 | df-pw 3673 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
| 4 | 1, 2, 3 | elab2 2967 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
| Colors of variables: wff set class |
| Syntax hints: ↔ wb 105 ∈ wcel 2205 Vcvv 2815 ⊆ wss 3213 𝒫 cpw 3671 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-ext 2216 |
| This theorem depends on definitions: df-bi 117 df-tru 1401 df-nf 1510 df-sb 1812 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-v 2817 df-in 3219 df-ss 3226 df-pw 3673 |
| This theorem is referenced by: velpw 3678 elpwg 3679 prsspw 3871 pwprss 3912 pwtpss 3913 pwv 3915 sspwuni 4078 iinpw 4084 iunpwss 4085 0elpw 4279 pwuni 4307 snelpw 4330 sspwb 4334 ssextss 4338 pwin 4405 pwunss 4406 iunpw 4603 xpsspw 4864 ssenen 7107 pw1ne3 7542 3nsssucpw1 7548 ioof 10307 hashfibclem 11210 tgdom 14954 distop 14967 epttop 14972 resttopon 15053 txuni2 15138 umgrbien 16122 umgredg 16157 |
| Copyright terms: Public domain | W3C validator |