![]() |
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 2967 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 220 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 2560 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 3894 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 2613 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 116 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 = wceq 1243 ∈ 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: ssexd 3897 difexg 3898 rabexg 3900 elssabg 3902 elpw2g 3910 abssexg 3934 snexgOLD 3935 snexg 3936 sess1 4074 sess2 4075 trsuc 4159 unexb 4177 uniexb 4205 xpexg 4452 riinint 4593 dmexg 4596 rnexg 4597 resexg 4650 resiexg 4653 imaexg 4680 exse2 4699 cnvexg 4855 coexg 4862 fabexg 5077 f1oabexg 5138 relrnfvex 5193 fvexg 5194 sefvex 5196 mptfvex 5256 mptexg 5386 ofres 5725 resfunexgALT 5737 cofunexg 5738 fnexALT 5740 f1dmex 5743 oprabexd 5754 mpt2exxg 5833 tposexg 5873 frecabex 5984 erex 6130 ssdomg 6258 fiprc 6292 shftfvalg 9419 shftfval 9422 |
Copyright terms: Public domain | W3C validator |