![]() |
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 3178 | . 2 ⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | df-pw 3577 | . 2 ⊢ 𝒫 𝐵 = {𝑥 ∣ 𝑥 ⊆ 𝐵} | |
4 | 1, 2, 3 | elab2 2885 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∈ wcel 2148 Vcvv 2737 ⊆ wss 3129 𝒫 cpw 3575 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-in 3135 df-ss 3142 df-pw 3577 |
This theorem is referenced by: velpw 3582 elpwg 3583 prsspw 3765 pwprss 3805 pwtpss 3806 pwv 3808 sspwuni 3970 iinpw 3976 iunpwss 3977 0elpw 4163 pwuni 4191 snelpw 4212 sspwb 4215 ssextss 4219 pwin 4281 pwunss 4282 iunpw 4479 xpsspw 4737 ssenen 6847 pw1ne3 7225 3nsssucpw1 7231 ioof 9966 tgdom 13434 distop 13447 epttop 13452 resttopon 13533 txuni2 13618 |
Copyright terms: Public domain | W3C validator |