| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode 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 2703 (a.k.a. Subset Axiom). |
| Ref | Expression |
|---|---|
| ssex.1 |
|
| Ref | Expression |
|---|---|
| ssex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ss 2053 |
. 2
| |
| 2 | ssex.1 |
. . . 4
| |
| 3 | 2 | inex2 2717 |
. . 3
|
| 4 | eleq1 1534 |
. . 3
| |
| 5 | 3, 4 | mpbii 193 |
. 2
|
| 6 | 1, 5 | sylbi 199 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: ssexi 2720 ssexg 2721 intex 2729 elpm 4336 mapss 4346 inf3lem7 4619 omex 4627 unbnnt 4639 bndrank 4682 scottex 4716 zorn2lem4 4791 ondomon 4856 elnp 5092 suplem2pr 5162 lbinfm 6048 elcncf 7265 unbenlem 7504 lpval 7743 lmclim 7963 sh 9078 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-12 968 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-sep 2703 |
| This theorem depends on definitions: df-bi 147 df-an 225 df-ex 981 df-sb 1172 df-clab 1464 df-cleq 1469 df-clel 1472 df-v 1812 df-in 2051 df-ss 2053 |