![]() |
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 5296 (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 | dfss2 3966 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
2 | ssex.1 | . . . 4 ⊢ 𝐵 ∈ V | |
3 | 2 | inex2 5315 | . . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V |
4 | eleq1 2814 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V)) | |
5 | 3, 4 | mpbii 232 | . 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V) |
6 | 1, 5 | sylbi 216 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 Vcvv 3464 ∩ cin 3947 ⊆ wss 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5296 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3421 df-v 3466 df-in 3955 df-ss 3965 |
This theorem is referenced by: ssexi 5319 ssexg 5320 intex 5336 moabex 5457 naddunif 8714 ixpiunwdom 9625 omex 9678 tcss 9779 bndrank 9876 scottex 9920 aceq3lem 10155 cfslb 10299 dcomex 10480 axdc2lem 10481 grothpw 10859 grothpwex 10860 grothomex 10862 elnp 11020 negfi 12208 hashfacenOLD 14466 limsuple 15474 limsuplt 15475 limsupbnd1 15478 o1add2 15620 o1mul2 15621 o1sub2 15622 o1dif 15626 caucvgrlem 15671 fsumo1 15810 lcmfval 16616 lcmf0val 16617 unbenlem 16904 ressbas2 17245 prdsval 17464 prdsbas 17466 rescbas 17839 rescbasOLD 17840 reschom 17841 rescco 17843 resccoOLD 17844 acsmapd 18573 issstrmgm 18640 issubmgm2 18690 issubmnd 18748 eqgfval 19165 dfod2 19557 ablfac1b 20065 islinds2 21806 pmatcollpw3lem 22772 2basgen 22980 prdstopn 23619 ressust 24255 rectbntr0 24835 elcncf 24896 cncfcnvcn 24933 cmssmscld 25365 cmsss 25366 ovolctb2 25508 limcfval 25888 ellimc2 25893 limcflf 25897 limcres 25902 limcun 25911 dvfval 25913 lhop2 26035 taylfval 26382 ulmval 26405 xrlimcnp 26992 axtgcont1 28391 fpwrelmap 32646 ressnm 32830 ressprs 32835 ordtrestNEW 33748 ddeval1 34079 ddeval0 34080 carsgclctunlem3 34166 bnj849 34782 msrval 35378 mclsval 35403 brsset 35725 isfne4 36064 refssfne 36082 topjoin 36089 bj-snglex 36692 mblfinlem3 37372 filbcmb 37453 cnpwstotbnd 37510 ismtyval 37513 ispsubsp 39456 ispsubclN 39648 isnumbasgrplem2 42801 rtrclex 43320 brmptiunrelexpd 43386 iunrelexp0 43405 mulcncff 45526 subcncff 45536 addcncff 45540 cncfuni 45542 divcncff 45547 etransclem1 45891 etransclem4 45894 etransclem13 45903 isvonmbl 46294 isubgriedg 47465 isubgrvtx 47467 uhgrimisgrgric 47513 linccl 47832 ellcoellss 47853 elbigolo1 47980 |
Copyright terms: Public domain | W3C validator |