![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluz | Unicode version |
Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
Ref | Expression |
---|---|
eluz |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluz1 8781 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | baibd 866 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3917 ax-pow 3969 ax-pr 3993 ax-cnex 7206 ax-resscn 7207 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 df-rex 2359 df-rab 2362 df-v 2613 df-sbc 2826 df-un 2987 df-in 2989 df-ss 2996 df-pw 3403 df-sn 3423 df-pr 3424 df-op 3426 df-uni 3623 df-br 3807 df-opab 3861 df-mpt 3862 df-id 4077 df-xp 4398 df-rel 4399 df-cnv 4400 df-co 4401 df-dm 4402 df-iota 4918 df-fun 4955 df-fv 4961 df-ov 5568 df-neg 7426 df-z 8510 df-uz 8778 |
This theorem is referenced by: uzneg 8795 uztric 8798 uzm1 8807 eluzdc 8855 fzn 9214 fzsplit2 9222 fznn 9259 uzsplit 9262 elfz2nn0 9282 fzouzsplit 9342 exfzdc 9403 fzfig 9589 faclbnd 9842 cvg1nlemcau 10096 cvg1nlemres 10097 zsupcllemstep 10573 zsupcl 10575 infssuzex 10577 uzdcinzz 10893 |
Copyright terms: Public domain | W3C validator |