![]() |
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 5057 (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 3838 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
2 | ssex.1 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 2 | inex2 5076 | . . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | eleq1 2848 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V)) | |
5 | 3, 4 | mpbii 225 | . 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V) |
6 | 1, 5 | sylbi 209 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∈ wcel 2051 Vcvv 3410 ∩ cin 3823 ⊆ wss 3824 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2745 ax-sep 5057 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-v 3412 df-in 3831 df-ss 3838 |
This theorem is referenced by: ssexi 5079 ssexg 5080 intex 5093 moabex 5205 ixpiunwdom 8849 omex 8899 tcss 8979 bndrank 9063 scottex 9107 aceq3lem 9339 cfslb 9485 dcomex 9666 axdc2lem 9667 grothpw 10045 grothpwex 10046 grothomex 10048 elnp 10206 negfi 11389 hashfacen 13624 limsuple 14695 limsuplt 14696 limsupbnd1 14699 o1add2 14840 o1mul2 14841 o1sub2 14842 o1dif 14846 caucvgrlem 14889 fsumo1 15026 lcmfval 15820 lcmf0val 15821 unbenlem 16099 ressbas2 16410 prdsval 16583 prdsbas 16585 rescbas 16970 reschom 16971 rescco 16973 acsmapd 17659 issstrmgm 17733 issubmnd 17799 eqgfval 18124 dfod2 18465 ablfac1b 18955 islinds2 20675 pmatcollpw3lem 21111 2basgen 21318 prdstopn 21956 ressust 22592 rectbntr0 23159 elcncf 23216 cncfcnvcn 23248 cmssmscld 23672 cmsss 23673 ovolctb2 23812 limcfval 24189 ellimc2 24194 limcflf 24198 limcres 24203 limcun 24212 dvfval 24214 lhop2 24331 taylfval 24666 ulmval 24687 xrlimcnp 25264 axtgcont1 25972 fpwrelmap 30246 ressnm 30397 ressprs 30401 ordtrestNEW 30841 ddeval1 31171 ddeval0 31172 carsgclctunlem3 31256 bnj849 31877 msrval 32338 mclsval 32363 brsset 32904 isfne4 33242 refssfne 33260 topjoin 33267 bj-snglex 33836 mblfinlem3 34405 filbcmb 34490 cnpwstotbnd 34550 ismtyval 34553 ispsubsp 36359 ispsubclN 36551 isnumbasgrplem2 39134 rtrclex 39374 brmptiunrelexpd 39425 iunrelexp0 39444 mulcncff 41611 subcncff 41623 addcncff 41627 cncfuni 41629 divcncff 41634 etransclem1 41981 etransclem4 41984 etransclem13 41993 isvonmbl 42381 issubmgm2 43455 linccl 43866 ellcoellss 43887 elbigolo1 44015 |
Copyright terms: Public domain | W3C validator |