Intuitionistic Logic Explorer |
This is the GIF version. Change to Unicode version |
Ref | Expression (see link for any distinct variable requirements) |
wn 3 | |
wi 4 | |
ax-1 5 | |
ax-2 6 | |
ax-mp 7 | |
wa 97 | |
wb 98 | |
ax-ia1 99 | |
ax-ia2 100 | |
ax-ia3 101 | |
df-bi 110 | |
ax-in1 544 | |
ax-in2 545 | |
wo 629 | |
ax-io 630 | |
wstab 739 | STAB |
df-stab 740 | STAB |
wdc 742 | DECID |
df-dc 743 | DECID |
w3o 884 | |
w3a 885 | |
df-3or 886 | |
df-3an 887 | |
wal 1241 | |
cv 1242 | |
wceq 1243 | |
wtru 1244 | |
df-tru 1246 | |
wfal 1248 | |
df-fal 1249 | |
wxo 1266 | |
df-xor 1267 | |
ax-5 1336 | |
ax-7 1337 | |
ax-gen 1338 | |
wnf 1349 | |
df-nf 1350 | |
wex 1381 | |
ax-ie1 1382 | |
ax-ie2 1383 | |
wcel 1393 | |
ax-8 1395 | |
ax-10 1396 | |
ax-11 1397 | |
ax-i12 1398 | |
ax-bndl 1399 | |
ax-4 1400 | |
ax-13 1404 | |
ax-14 1405 | |
ax-17 1419 | |
ax-i9 1423 | |
ax-ial 1427 | |
ax-i5r 1428 | |
ax-10o 1604 | |
wsb 1645 | |
df-sb 1646 | |
ax-16 1695 | |
ax-11o 1704 | |
weu 1900 | |
wmo 1901 | |
df-eu 1903 | |
df-mo 1904 | |
ax-ext 2022 | |
cab 2026 | |
df-clab 2027 | |
df-cleq 2033 | |
df-clel 2036 | |
wnfc 2165 | |
df-nfc 2167 | |
wne 2204 | |
wnel 2205 | |
df-ne 2206 | |
df-nel 2207 | |
wral 2306 | |
wrex 2307 | |
wreu 2308 | |
wrmo 2309 | |
crab 2310 | |
df-ral 2311 | |
df-rex 2312 | |
df-reu 2313 | |
df-rmo 2314 | |
df-rab 2315 | |
cvv 2557 | |
df-v 2559 | |
wcdeq 2747 | CondEq |
df-cdeq 2748 | CondEq |
wsbc 2764 | |
df-sbc 2765 | |
csb 2852 | |
df-csb 2853 | |
cdif 2914 | |
cun 2915 | |
cin 2916 | |
wss 2917 | |
wpss 2918 | |
df-dif 2920 | |
df-un 2922 | |
df-in 2924 | |
df-ss 2931 | |
df-pss 2933 | |
c0 3224 | |
df-nul 3225 | |
cif 3331 | |
df-if 3332 | |
cpw 3359 | |
df-pw 3361 | |
csn 3375 | |
cpr 3376 | |
ctp 3377 | |
cop 3378 | |
cotp 3379 | |
df-sn 3381 | |
df-pr 3382 | |
df-tp 3383 | |
df-op 3384 | |
df-ot 3385 | |
cuni 3580 | |
df-uni 3581 | |
cint 3615 | |
df-int 3616 | |
ciun 3657 | |
ciin 3658 | |
df-iun 3659 | |
df-iin 3660 | |
wdisj 3745 | Disj |
df-disj 3746 | Disj |
wbr 3764 | |
df-br 3765 | |
copab 3817 | |
cmpt 3818 | |
df-opab 3819 | |
df-mpt 3820 | |
wtr 3854 | |
df-tr 3855 | |
ax-coll 3872 | |
ax-sep 3875 | |
ax-nul 3883 | |
ax-pow 3927 | |
ax-pr 3944 | |
cep 4024 | |
cid 4025 | |
df-eprel 4026 | |
df-id 4030 | |
wpo 4031 | |
wor 4032 | |
df-po 4033 | |
df-iso 4034 | |
wfrfor 4064 | FrFor |
wfr 4065 | |
wse 4066 | Se |
wwe 4067 | |
df-frfor 4068 | FrFor |
df-frind 4069 | FrFor |
df-se 4070 | Se |
df-wetr 4071 | |
word 4099 | |
con0 4100 | |
wlim 4101 | |
csuc 4102 | |
df-iord 4103 | |
df-on 4105 | |
df-ilim 4106 | |
df-suc 4108 | |
ax-un 4170 | |
ax-setind 4262 | |
ax-iinf 4311 | |
com 4313 | |
df-iom 4314 | |
cxp 4343 | |
ccnv 4344 | |
cdm 4345 | |
crn 4346 | |
cres 4347 | |
cima 4348 | |
ccom 4349 | |
wrel 4350 | |
df-xp 4351 | |
df-rel 4352 | |
df-cnv 4353 | |
df-co 4354 | |
df-dm 4355 | |
df-rn 4356 | |
df-res 4357 | |
df-ima 4358 | |
cio 4865 | |
df-iota 4867 | |
wfun 4896 | |
wfn 4897 | |
wf 4898 | |
wf1 4899 | |
wfo 4900 | |
wf1o 4901 | |
cfv 4902 | |
wiso 4903 | |
df-fun 4904 | |
df-fn 4905 | |
df-f 4906 | |
df-f1 4907 | |
df-fo 4908 | |
df-f1o 4909 | |
df-fv 4910 | |
df-isom 4911 | |
crio 5467 | |
df-riota 5468 | |
co 5512 | |
coprab 5513 | |
cmpt2 5514 | |
df-ov 5515 | |
df-oprab 5516 | |
df-mpt2 5517 | |
cof 5710 | |
cofr 5711 | |
df-of 5712 | |
df-ofr 5713 | |
c1st 5765 | |
c2nd 5766 | |
df-1st 5767 | |
df-2nd 5768 | |
ctpos 5859 | tpos |
df-tpos 5860 | tpos |
wsmo 5900 | |
df-smo 5901 | |
crecs 5919 | recs |
df-recs 5920 | recs |
crdg 5956 | |
df-irdg 5957 | recs |
cfrec 5977 | frec |
df-frec 5978 | frec recs |
c1o 5994 | |
c2o 5995 | |
c3o 5996 | |
c4o 5997 | |
coa 5998 | |
comu 5999 | |
coei 6000 | ↑𝑜 |
df-1o 6001 | |
df-2o 6002 | |
df-3o 6003 | |
df-4o 6004 | |
df-oadd 6005 | |
df-omul 6006 | |
df-oexpi 6007 | ↑𝑜 |
wer 6103 | |
cec 6104 | |
cqs 6105 | |
df-er 6106 | |
df-ec 6108 | |
df-qs 6112 | |
cen 6219 | |
cdom 6220 | |
cfn 6221 | |
df-en 6222 | |
df-dom 6223 | |
df-fin 6224 | |
ccrd 6359 | |
df-card 6360 | |
cnpi 6370 | |
cpli 6371 | |
cmi 6372 | |
clti 6373 | |
cplpq 6374 | |
cmpq 6375 | |
cltpq 6376 | |
ceq 6377 | |
cnq 6378 | |
c1q 6379 | |
cplq 6380 | |
cmq 6381 | |
crq 6382 | |
cltq 6383 | |
ceq0 6384 | ~Q0 |
cnq0 6385 | Q0 |
c0q0 6386 | 0Q0 |
cplq0 6387 | +Q0 |
cmq0 6388 | ·Q0 |
cnp 6389 | |
c1p 6390 | |
cpp 6391 | |
cmp 6392 | |
cltp 6393 | |
cer 6394 | |
cnr 6395 | |
c0r 6396 | |
c1r 6397 | |
cm1r 6398 | |
cplr 6399 | |
cmr 6400 | |
cltr 6401 | |
df-ni 6402 | |
df-pli 6403 | |
df-mi 6404 | |
df-lti 6405 | |
df-plpq 6442 | |
df-mpq 6443 | |
df-ltpq 6444 | |
df-enq 6445 | |
df-nqqs 6446 | |
df-plqqs 6447 | |
df-mqqs 6448 | |
df-1nqqs 6449 | |
df-rq 6450 | |
df-ltnqqs 6451 | |
df-enq0 6522 | ~Q0 |
df-nq0 6523 | Q0 ~Q0 |
df-0nq0 6524 | 0Q0 ~Q0 |
df-plq0 6525 | +Q0 Q0 Q0 ~Q0 ~Q0 ~Q0 |
df-mq0 6526 | ·Q0 Q0 Q0 ~Q0 ~Q0 ~Q0 |
df-inp 6564 | |
df-i1p 6565 | |
df-iplp 6566 | |
df-imp 6567 | |
df-iltp 6568 | |
df-enr 6811 | |
df-nr 6812 | |
df-plr 6813 | |
df-mr 6814 | |
df-ltr 6815 | |
df-0r 6816 | |
df-1r 6817 | |
df-m1r 6818 | |
cc 6887 | |
cr 6888 | |
cc0 6889 | |
c1 6890 | |
ci 6891 | |
caddc 6892 | |
cltrr 6893 | |
cmul 6894 | |
df-c 6895 | |
df-0 6896 | |
df-1 6897 | |
df-i 6898 | |
df-r 6899 | |
df-add 6900 | |
df-mul 6901 | |
df-lt 6902 | |
ax-cnex 6975 | |
ax-resscn 6976 | |
ax-1cn 6977 | |
ax-1re 6978 | |
ax-icn 6979 | |
ax-addcl 6980 | |
ax-addrcl 6981 | |
ax-mulcl 6982 | |
ax-mulrcl 6983 | |
ax-addcom 6984 | |
ax-mulcom 6985 | |
ax-addass 6986 | |
ax-mulass 6987 | |
ax-distr 6988 | |
ax-i2m1 6989 | |
ax-1rid 6991 | |
ax-0id 6992 | |
ax-rnegex 6993 | |
ax-precex 6994 | |
ax-cnre 6995 | |
ax-pre-ltirr 6996 | |
ax-pre-ltwlin 6997 | |
ax-pre-lttrn 6998 | |
ax-pre-apti 6999 | |
ax-pre-ltadd 7000 | |
ax-pre-mulgt0 7001 | |
ax-pre-mulext 7002 | |
ax-arch 7003 | |
ax-caucvg 7004 | |
cpnf 7057 | |
cmnf 7058 | |
cxr 7059 | |
clt 7060 | |
cle 7061 | |
df-pnf 7062 | |
df-mnf 7063 | |
df-xr 7064 | |
df-ltxr 7065 | |
df-le 7066 | |
cmin 7182 | |
cneg 7183 | |
df-sub 7184 | |
df-neg 7185 | |
creap 7565 | #ℝ |
df-reap 7566 | #ℝ |
cap 7572 | # |
df-ap 7573 | # #ℝ #ℝ |
cdiv 7651 | |
df-div 7652 | |
cn 7914 | |
df-inn 7915 | |
c2 7964 | |
c3 7965 | |
c4 7966 | |
c5 7967 | |
c6 7968 | |
c7 7969 | |
c8 7970 | |
c9 7971 | |
c10 7972 | |
df-2 7973 | |
df-3 7974 | |
df-4 7975 | |
df-5 7976 | |
df-6 7977 | |
df-7 7978 | |
df-8 7979 | |
df-9 7980 | |
df-10 7981 | |
cn0 8181 | |
df-n0 8182 | |
cz 8245 | |
df-z 8246 | |
cdc 8368 | ; |
df-dec 8369 | ; |
cuz 8473 | |
df-uz 8474 | |
cq 8554 | |
df-q 8555 | |
crp 8583 | |
df-rp 8584 | |
cxne 8686 | |
cxad 8687 | |
cxmu 8688 | |
df-xneg 8689 | |
df-xadd 8690 | |
df-xmul 8691 | |
cioo 8757 | |
cioc 8758 | |
cico 8759 | |
cicc 8760 | |
df-ioo 8761 | |
df-ioc 8762 | |
df-ico 8763 | |
df-icc 8764 | |
cfz 8874 | |
df-fz 8875 | |
cfzo 8999 | ..^ |
df-fzo 9000 | ..^ |
cfl 9112 | |
cceil 9113 | ⌈ |
df-fl 9114 | |
df-ceil 9115 | ⌈ |
cmo 9164 | |
df-mod 9165 | |
cseq 9211 | |
df-iseq 9212 | frec |
cexp 9254 | |
df-iexp 9255 | |
cshi 9415 | |
df-shft 9416 | |
ccj 9439 | |
cre 9440 | |
cim 9441 | |
df-cj 9442 | |
df-re 9443 | |
df-im 9444 | |
csqrt 9594 | |
cabs 9595 | |
df-rsqrt 9596 | |
df-abs 9597 | |
cli 9799 | |
df-clim 9800 | |
csu 9872 | |
df-sum 9873 | |
The list of syntax, axioms (ax-) and definitions (df-) for the starts here | |
wbd 9932 | BOUNDED |
ax-bd0 9933 | BOUNDED BOUNDED |
ax-bdim 9934 | BOUNDED BOUNDED BOUNDED |
ax-bdan 9935 | BOUNDED BOUNDED BOUNDED |
ax-bdor 9936 | BOUNDED BOUNDED BOUNDED |
ax-bdn 9937 | BOUNDED BOUNDED |
ax-bdal 9938 | BOUNDED BOUNDED |
ax-bdex 9939 | BOUNDED BOUNDED |
ax-bdeq 9940 | BOUNDED |
ax-bdel 9941 | BOUNDED |
ax-bdsb 9942 | BOUNDED BOUNDED |
wbdc 9960 | BOUNDED |
df-bdc 9961 | BOUNDED BOUNDED |
ax-bdsep 10004 | BOUNDED |
ax-bj-d0cl 10044 | BOUNDED DECID |
wind 10050 | Ind |
df-bj-ind 10051 | Ind |
ax-infvn 10066 | Ind Ind |
ax-bdsetind 10093 | BOUNDED |
ax-inf2 10101 | |
ax-strcoll 10107 | |
ax-sscoll 10112 | |
ax-ddkcomp 10114 | |
walsi 10115 | ! |
walsc 10116 | ! |
df-alsi 10117 | ! |
df-alsc 10118 | ! |
Copyright terms: Public domain | W3C validator |