![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssex | Structured version Visualization version GIF version |
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 5167 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
ssex.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
ssex | ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ss 3898 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
2 | ssex.1 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 2 | inex2 5186 | . . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | eleq1 2877 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V)) | |
5 | 3, 4 | mpbii 236 | . 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V) |
6 | 1, 5 | sylbi 220 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 Vcvv 3441 ∩ cin 3880 ⊆ wss 3881 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-in 3888 df-ss 3898 |
This theorem is referenced by: ssexi 5190 ssexg 5191 intex 5204 moabex 5316 ixpiunwdom 9038 omex 9090 tcss 9170 bndrank 9254 scottex 9298 aceq3lem 9531 cfslb 9677 dcomex 9858 axdc2lem 9859 grothpw 10237 grothpwex 10238 grothomex 10240 elnp 10398 negfi 11577 hashfacen 13808 limsuple 14827 limsuplt 14828 limsupbnd1 14831 o1add2 14972 o1mul2 14973 o1sub2 14974 o1dif 14978 caucvgrlem 15021 fsumo1 15159 lcmfval 15955 lcmf0val 15956 unbenlem 16234 ressbas2 16547 prdsval 16720 prdsbas 16722 rescbas 17091 reschom 17092 rescco 17094 acsmapd 17780 issstrmgm 17855 issubmnd 17930 eqgfval 18320 dfod2 18683 ablfac1b 19185 islinds2 20502 pmatcollpw3lem 21388 2basgen 21595 prdstopn 22233 ressust 22870 rectbntr0 23437 elcncf 23494 cncfcnvcn 23530 cmssmscld 23954 cmsss 23955 ovolctb2 24096 limcfval 24475 ellimc2 24480 limcflf 24484 limcres 24489 limcun 24498 dvfval 24500 lhop2 24618 taylfval 24954 ulmval 24975 xrlimcnp 25554 axtgcont1 26262 fpwrelmap 30495 ressnm 30664 ressprs 30668 ordtrestNEW 31274 ddeval1 31603 ddeval0 31604 carsgclctunlem3 31688 bnj849 32307 msrval 32898 mclsval 32923 brsset 33463 isfne4 33801 refssfne 33819 topjoin 33826 bj-snglex 34409 mblfinlem3 35096 filbcmb 35178 cnpwstotbnd 35235 ismtyval 35238 ispsubsp 37041 ispsubclN 37233 isnumbasgrplem2 40048 rtrclex 40317 brmptiunrelexpd 40384 iunrelexp0 40403 mulcncff 42512 subcncff 42522 addcncff 42526 cncfuni 42528 divcncff 42533 etransclem1 42877 etransclem4 42880 etransclem13 42889 isvonmbl 43277 issubmgm2 44410 linccl 44823 ellcoellss 44844 elbigolo1 44971 |
Copyright terms: Public domain | W3C validator |