Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssexg | GIF version |
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
ssexg | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3161 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 230 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 2724 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 4113 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 2781 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 124 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1342 ∈ wcel 2135 Vcvv 2721 ⊆ wss 3111 |
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 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-sep 4094 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-in 3117 df-ss 3124 |
This theorem is referenced by: ssexd 4116 difexg 4117 rabexg 4119 elssabg 4121 elpw2g 4129 abssexg 4155 snexg 4157 sess1 4309 sess2 4310 trsuc 4394 unexb 4414 abnexg 4418 uniexb 4445 xpexg 4712 riinint 4859 dmexg 4862 rnexg 4863 resexg 4918 resiexg 4923 imaexg 4952 exse2 4972 cnvexg 5135 coexg 5142 fabexg 5369 f1oabexg 5438 relrnfvex 5498 fvexg 5499 sefvex 5501 mptfvex 5565 mptexg 5704 ofres 6058 resfunexgALT 6070 cofunexg 6071 fnexALT 6073 f1dmex 6076 oprabexd 6087 mpoexxg 6170 tposexg 6217 frecabex 6357 erex 6516 mapex 6611 pmvalg 6616 elpmg 6621 elmapssres 6630 pmss12g 6632 ixpexgg 6679 ssdomg 6735 fiprc 6772 fival 6926 iccen 9933 shftfvalg 10746 shftfval 10749 toponsspwpwg 12561 tgval 12590 tgvalex 12591 eltg 12593 eltg2 12594 tgss 12604 basgen2 12622 bastop1 12624 topnex 12627 resttopon 12712 restabs 12716 lmfval 12733 cnrest 12776 txss12 12807 metrest 13047 dvbss 13195 dvcnp2cntop 13204 dvaddxxbr 13206 dvmulxxbr 13207 |
Copyright terms: Public domain | W3C validator |