NFE Home New Foundations Explorer This is the GIF version.
Change to Unicode version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3
wi 4
ax-1 5
ax-2 6
ax-3 7
ax-mp 8    &       =>   
wb 173
df-bi 174
wo 354
wa 355
df-or 356
df-an 357
w3o 883
w3a 884
df-3or 885
df-3an 886
ax-meredith 1230
wnand 1258
df-nand 1259
wtru 1298
wfal 1299
df-tru 1301
df-fal 1302
wal 1322
ax-5 1323
ax-6 1324
ax-7 1325
ax-gen 1326    =>   
wex 1327
df-ex 1328
cv 1397
wceq 1398
wcel 1400
ax-8 1402
ax-10 1403
ax-11 1404
ax-12 1405
ax-13 1406
ax-14 1407
ax-17 1413
ax-9 1424
ax-4 1429
ax-5o 1431
ax-6o 1434
ax-9o 1519
ax-10o 1538
wsbc 1566
df-sb 1568
ax-16 1606
ax-11o 1616
ax-15 1769
weu 1791
wmo 1792
df-eu 1795
df-mo 1796
ax-ext 1877
cab 1882
df-clab 1883
df-cleq 1888    =>   
df-clel 1891
wne 2012
wnel 2013
df-ne 2014
df-nel 2015
wral 2103
wrex 2104
wreu 2105
crab 2106
df-ral 2107
df-rex 2108
df-reu 2109
df-rab 2110
cvv 2300
df-v 2302
df-sbc 2469
csb 2550
df-csb 2551
cnin 2606 &ncap
ccompl 2607
cdif 2608
cun 2609
cin 2610
csymdif 2611
df-nin 2613 &ncap
df-compl 2614 &ncap
df-in 2615 &ncap
df-un 2616 &ncap ∼
df-dif 2617
df-symdif 2618
c0 2726
df-nul 2727
csn 2803
cpr 2804
ctp 2805
df-sn 2807
df-pr 2808
df-tp 2809
copk 2862
df-opk 2863
wss 2874
wpss 2875
df-ss 2876
df-pss 2878
cuni 3037
df-uni 3038
cint 3071
df-int 3072
cif 3108
df-if 3109
cpw 3165
df-pw 3167
ax-nin 3180
ax-xp 3181
ax-cnv 3182
ax-1c 3183
ax-sset 3184
ax-si 3185
ax-ins2 3186
ax-ins3 3187
ax-typlower 3188
ax-sn 3189
cuni1 32371
c1c 3238 1c
cpw1 3239 1
df-1c 3240 1c
df-pw1 3241 1 1c
df-uni1 32421 1c
cxpk 3278 k
ccnvk 3279 k
cins2k 3280 Ins2k
cins3k 3281 Ins3k
cp6 3282 P6
cimak 3283 k
ccomk 3284 k
csik 3285 SIk
cimagek 3286 Imagek
cssetk 3287 SSetk
cidk 3288 k
df-xpk 3289 k
df-cnvk 3290 k
df-ins2k 3291 Ins2k
df-ins3k 3292 Ins3k
df-imak 3293 k
df-cok 3294 k Ins2k Ins3k kk
df-p6 3295 P6 k
df-sik 3296 SIk
df-ssetk 3297 SSetk
df-imagek 3298 Imagek k Ins2k SSetk Ins3k SSetk k k SIk k111c
df-idk 3299 k
cio 3448
df-iota 3450
cnnc 3481 Nn
c0c 3482 0c
cplc 3483
cfin 3484 Fin
df-0c 3485 0c
df-addc 3486
df-nnc 3487 Nn 0c 1c
df-fin 3488 Fin Nn
clefin 3539 <_fin
cltfin 3540 <fin
cncfin 3541 Ncfin
ctfin 3542 Tfin
cevenfin 3543 Evenfin
coddfin 3544 Oddfin
wsfin 3545 Sfin
cspfin 3546 Spfin
df-lefin 3547 <_fin Nn
df-ltfin 3548 <fin Nn 1c
df-ncfin 3549 Ncfin Nn
df-tfin 3550 Tfin Nn 1
df-evenfin 3551 Evenfin Nn
df-oddfin 3552 Oddfin Nn 1c
df-sfin 3553 Sfin Nn Nn 1
df-spfin 3554 Spfin Ncfin Sfin
cop 3669
cphi 3670 Phi
cproj1 3671 Proj1
cproj2 3672 Proj2
df-phi 3673 Phi Nn 1c
df-op 3674 Phi Phi 0c
df-proj1 3675 Proj1 Phi
df-proj2 3676 Proj2 Phi 0c
copab 3722
df-opab 3723
wbr 3736
df-br 3737
c1st 3815
cswap 3816 Swap
csset 3817 SSet
csi 3818 SI
ccom 3819
cima 3820
df-1st 3821
df-swap 3822 Swap
df-sset 3823 SSet
df-co 3824
df-ima 3825
df-si 3826 SI
ciun 3860
ciin 3861
df-iun 3862
df-iin 3863
cep 3934
cid 3935
df-eprel 3936
df-id 3939
cxp 3942
ccnv 3943
cdm 3944
crn 3945
cres 3946
wrel 3947
wfun 3948
wfn 3949
wf 3950
wf1 3951
wfo 3952
wf1o 3953
cfv 3954
wiso 3955
c2nd 3956
df-xp 3957
df-rel 3958
df-cnv 3959
df-rn 3960
df-dm 3961
df-res 3962
df-fun 3963
df-fn 3964
df-f 3965
df-f1 3966
df-fo 3967
df-f1o 3968
df-fv 3969
df-iso 3970
df-2nd 3971
co 4766
copab2 4767
df-ov 4768
df-oprab 4769
cmpt 4893
cmpt2 4894
df-mpt 4895
df-mpt2 4896
ctxp 4962
cpprod 4963 PProd
cfix 4964
cimage 4965 Image
ccup 4966 Cup
cdisj 4967 Disj
caddcfn 4968 AddC
cins2 4969 Ins2
cins3 4970 Ins3
cins4 4971 Ins4
csi3 4972 SI3
cfuns 4973 Funs
cfns 4974 Fns
ccross 4975 Cross
cpw1fn 4976 Pw1Fn
cfullfun 4977 FullFun
df-txp 4978
df-pprod 4979 PProd
df-fix 4980
df-cup 4981 Cup
df-disj 4982 Disj
df-addcfn 4983 AddC
df-ins2 4984 Ins2
df-ins3 4985 Ins3
df-image 4986 Image Ins2 SSet Ins3 SSet SI 1c
df-ins4 4987 Ins4
df-si3 4988 SI3 SI SI SI 1
df-funs 4989 Funs
df-fns 4990 Fns
df-cross 4991 Cross
df-pw1fn 4992 Pw1Fn 1c 1
df-fullfun 4993 FullFun
cclos1 5085 Clos1
df-clos1 5086 Clos1
ctrans 5099 Trans
cref 5100 Ref
cantisym 5101 Antisym
cpartial 5102 Po
cconnex 5103 Connex
cstrict 5104 Or
cfound 5105 Fr
cwe 5106 We
cext 5107 Ext
csym 5108 Sym
cer 5109 Er
df-trans 5110 Trans
df-ref 5111 Ref
df-antisym 5112 Antisym
df-partial 5113 Po Ref Trans Antisym
df-connex 5114 Connex
df-strict 5115 Or Po Connex
df-found 5116 Fr
df-we 5117 We Or Fr
df-ext 5118 Ext
df-sym 5119 Sym
df-er 5120 Er Sym Trans
cec 5156
cqs 5157
df-ec 5158
df-qs 5162
cmap 5211
cpm 5212
df-map 5213
df-pm 5214
cen 5240
df-en 5241
cncs 5300 NC
clec 5301 <_c
cltc 5302 <c
cnc 5303 Nc
cmuc 5304 ·c
ctc 5305 Tc
c2c 5306 2c
c3c 5307 3c
cce 5308c
ctcfn 5309 TcFn
df-ncs 5310 NC
df-lec 5311 <_c
df-ltc 5312 <c <_c
df-nc 5313 Nc
df-muc 5314 ·c NC NC
df-tc 5315 Tc NC Nc 1
df-2c 5316 2c Nc
df-3c 5317 3c Nc
df-ce 5318c NC NC 1 1
df-tcfn 5319 TcFn 1c Tc
cspac 5465 Spac
df-spac 5466 Spac NC Clos1 NC NC 2cc
  Copyright terms: Public domain W3C validator