Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssexi | GIF version |
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Ref | Expression |
---|---|
ssexi.1 | ⊢ 𝐵 ∈ V |
ssexi.2 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
ssexi | ⊢ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexi.2 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | ssexi.1 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 2 | ssex 3894 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
4 | 1, 3 | ax-mp 7 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1393 Vcvv 2557 ⊆ wss 2917 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-v 2559 df-in 2924 df-ss 2931 |
This theorem is referenced by: zfausab 3899 pp0ex 3940 ord3ex 3941 epse 4079 opabex 5385 oprabex 5755 phplem2 6316 phpm 6327 niex 6410 enqex 6458 enq0ex 6537 npex 6571 ltnqex 6647 gtnqex 6648 recexprlemell 6720 recexprlemelu 6721 enrex 6822 axcnex 6935 peano5nnnn 6966 reex 7015 nnex 7920 zex 8254 qex 8567 ixxex 8768 frecuzrdgrrn 9194 frec2uzrdg 9195 frecuzrdgrom 9196 frecuzrdgsuc 9201 resqrexlemf 9605 resqrexlemf1 9606 resqrexlemfp1 9607 iserclim0 9826 climle 9854 |
Copyright terms: Public domain | W3C validator |