| 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 5294 (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 3968 | . 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) | |
| 2 | ssex.1 | . . . 4 ⊢ 𝐵 ∈ V | |
| 3 | 2 | inex2 5316 | . . 3 ⊢ (𝐴 ∩ 𝐵) ∈ V |
| 4 | eleq1 2828 | . . 3 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) ∈ V ↔ 𝐴 ∈ V)) | |
| 5 | 3, 4 | mpbii 233 | . 2 ⊢ ((𝐴 ∩ 𝐵) = 𝐴 → 𝐴 ∈ V) |
| 6 | 1, 5 | sylbi 217 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Vcvv 3479 ∩ cin 3949 ⊆ wss 3950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2707 ax-sep 5294 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-in 3957 df-ss 3967 |
| This theorem is referenced by: ssexi 5320 ssexg 5321 intex 5342 moabex 5462 naddunif 8727 ixpiunwdom 9626 omex 9679 tcss 9780 bndrank 9877 scottex 9921 aceq3lem 10156 cfslb 10302 dcomex 10483 axdc2lem 10484 grothpw 10862 grothpwex 10863 grothomex 10865 elnp 11023 negfi 12213 limsuple 15510 limsuplt 15511 limsupbnd1 15514 o1add2 15656 o1mul2 15657 o1sub2 15658 o1dif 15662 caucvgrlem 15705 fsumo1 15844 lcmfval 16654 lcmf0val 16655 unbenlem 16942 ressbas2 17279 prdsval 17496 prdsbas 17498 rescbas 17869 reschom 17870 rescco 17872 acsmapd 18595 issstrmgm 18662 issubmgm2 18712 issubmnd 18770 eqgfval 19190 dfod2 19578 ablfac1b 20086 islinds2 21825 pmatcollpw3lem 22779 2basgen 22987 prdstopn 23626 ressust 24262 rectbntr0 24844 elcncf 24905 cncfcnvcn 24942 cmssmscld 25374 cmsss 25375 ovolctb2 25517 limcfval 25897 ellimc2 25902 limcflf 25906 limcres 25911 limcun 25920 dvfval 25922 lhop2 26044 taylfval 26390 ulmval 26413 xrlimcnp 27001 axtgcont1 28466 fpwrelmap 32733 ressnm 32936 ressprs 32941 ordtrestNEW 33898 ddeval1 34213 ddeval0 34214 carsgclctunlem3 34300 bnj849 34917 msrval 35521 mclsval 35546 brsset 35868 isfne4 36319 refssfne 36337 topjoin 36344 bj-snglex 36952 mblfinlem3 37644 filbcmb 37725 cnpwstotbnd 37782 ismtyval 37785 ispsubsp 39725 ispsubclN 39917 isnumbasgrplem2 43094 rtrclex 43608 brmptiunrelexpd 43674 iunrelexp0 43693 mulcncff 45861 subcncff 45871 addcncff 45875 cncfuni 45877 divcncff 45882 etransclem1 46226 etransclem4 46229 etransclem13 46238 isvonmbl 46629 isubgriedg 47825 isubgrvtx 47829 uhgrimisgrgric 47875 linccl 48307 ellcoellss 48328 elbigolo1 48454 |
| Copyright terms: Public domain | W3C validator |