![]() |
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 4073 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1481 Vcvv 2689 ⊆ wss 3076 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-sep 4054 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-in 3082 df-ss 3089 |
This theorem is referenced by: zfausab 4078 pp0ex 4121 ord3ex 4122 epse 4272 opabex 5652 oprabex 6034 phplem2 6755 phpm 6767 snexxph 6846 sbthlem2 6854 niex 7144 enqex 7192 enq0ex 7271 npex 7305 ltnqex 7381 gtnqex 7382 recexprlemell 7454 recexprlemelu 7455 enrex 7569 axcnex 7691 peano5nnnn 7724 reex 7778 nnex 8750 zex 9087 qex 9451 ixxex 9712 iccen 9819 serclim0 11106 climle 11135 iserabs 11276 isumshft 11291 explecnv 11306 prodfclim1 11345 prmex 11830 exmidunben 11975 istopon 12219 dmtopon 12229 lmres 12456 climcncf 12779 reldvg 12856 |
Copyright terms: Public domain | W3C validator |