![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluzel2 | Unicode version |
Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
eluzel2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzf 8703 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | frel 5080 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
. . 3
![]() ![]() ![]() |
4 | relelfvdm 5237 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpan 415 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1 | fdmi 5082 |
. 2
![]() ![]() ![]() ![]() ![]() |
7 | 5, 6 | syl6eleq 2172 |
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 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-cnex 7129 ax-resscn 7130 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ral 2354 df-rex 2355 df-rab 2358 df-v 2604 df-sbc 2817 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-br 3794 df-opab 3848 df-mpt 3849 df-id 4056 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-rn 4382 df-res 4383 df-ima 4384 df-iota 4897 df-fun 4934 df-fn 4935 df-f 4936 df-fv 4940 df-ov 5546 df-neg 7349 df-z 8433 df-uz 8701 |
This theorem is referenced by: eluz2 8706 uztrn 8716 uzneg 8718 uzss 8720 uz11 8722 eluzadd 8728 uzm1 8730 uzin 8732 uzind4 8757 elfz5 9113 elfzel1 9120 eluzfz1 9126 fzsplit2 9145 fzopth 9155 fzpred 9163 fzpreddisj 9164 fzdifsuc 9174 uzsplit 9185 uzdisj 9186 elfzp12 9192 fzm1 9193 uznfz 9196 nn0disj 9225 fzolb 9239 fzoss2 9258 fzouzdisj 9266 ige2m2fzo 9284 elfzonelfzo 9316 frec2uzrand 9487 frecfzen2 9509 iseqcl 9537 iseqp1 9538 iseqp1t 9539 iseqfeq2 9545 iseqfveq 9546 iseqshft2 9548 iseqsplit 9554 iseqcaopr3 9556 iseqid3s 9562 iseqid 9563 iseqhomo 9565 iseqz 9566 serige0 9570 serile 9571 leexp2a 9626 rexanuz2 10015 cau4 10140 clim2iser 10313 clim2iser2 10314 climserile 10321 fisumcvg 10338 |
Copyright terms: Public domain | W3C validator |