![]() |
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 4155 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 Vcvv 2752 ⊆ wss 3144 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4136 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-in 3150 df-ss 3157 |
This theorem is referenced by: zfausab 4160 pp0ex 4204 ord3ex 4205 epse 4357 opabex 5757 mptexw 6133 oprabex 6148 mpoexw 6233 phplem2 6876 phpm 6888 snexxph 6974 sbthlem2 6982 2omotaplemst 7282 niex 7336 enqex 7384 enq0ex 7463 npex 7497 ltnqex 7573 gtnqex 7574 recexprlemell 7646 recexprlemelu 7647 enrex 7761 axcnex 7883 peano5nnnn 7916 reex 7970 nnex 8950 zex 9287 qex 9657 ixxex 9924 iccen 10031 serclim0 11340 climle 11369 iserabs 11510 isumshft 11525 explecnv 11540 prodfclim1 11579 prmex 12140 exmidunben 12472 prdsex 12767 znval 13925 znle 13926 znbaslemnn 13928 istopon 13950 dmtopon 13960 lmres 14185 climcncf 14508 reldvg 14585 |
Copyright terms: Public domain | W3C validator |