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 176
df-bi 177
wo 357
wa 358
df-or 359
df-an 360
w3o 933
w3a 934
df-3or 935
df-3an 936
wnan 1287
df-nan 1288
wxo 1304  \/_
df-xor 1305  \/_
wtru 1316
wfal 1317
df-tru 1319
df-fal 1320
whad 1378 hadd
wcad 1379 cadd
df-had 1380 hadd  \/_  \/_
df-cad 1381 cadd  \/_
ax-meredith 1406
wal 1540
wex 1541
df-ex 1542
wnf 1544 
F/
df-nf 1545  F/
ax-gen 1546    =>   
ax-5 1557
ax-17 1616
cv 1641
wceq 1642
wsb 1648
df-sb 1649
ax-9 1654
ax-8 1675
wcel 1710
ax-13 1712
ax-14 1714
ax-6 1729
ax-7 1734
ax-11 1746
ax-12 1925
ax-4 2135
ax-5o 2136
ax-6o 2137
ax-9o 2138
ax-10o 2139
ax-10 2140
ax-11o 2141
ax-12o 2142
ax-15 2143
ax-16 2144
weu 2204
wmo 2205
df-eu 2208
df-mo 2209
ax-7d 2295
ax-8d 2296
ax-9d1 2297
ax-9d2 2298
ax-10d 2299
ax-11d 2300
ax-ext 2334
cab 2339
df-clab 2340
df-cleq 2346    =>   
df-clel 2349
wnfc 2476 F/_
df-nfc 2478 F/_  F/
wne 2516
wnel 2517
df-ne 2518
df-nel 2519
wral 2614
wrex 2615
wreu 2616
wrmo 2617
crab 2618
df-ral 2619
df-rex 2620
df-reu 2621
df-rmo 2622
df-rab 2623
cvv 2859
df-v 2861
wsbc 3046 [. ].
df-sbc 3047 [. ].
csb 3136
df-csb 3137 [. ].
cnin 3204 &ncap
ccompl 3205
cdif 3206
cun 3207
cin 3208
csymdif 3209
df-nin 3211 &ncap
df-compl 3212 &ncap
df-in 3213 &ncap
df-un 3214 &ncap ∼
df-dif 3215
df-symdif 3216
wss 3257
wpss 3258
df-ss 3259
df-pss 3261
c0 3550
df-nul 3551
cif 3662
df-if 3663
cpw 3722
df-pw 3724
csn 3737
cpr 3738
ctp 3739
df-sn 3741
df-pr 3742
df-tp 3743
cuni 3891
df-uni 3892
cint 3926
df-int 3927
ciun 3969
ciin 3970
df-iun 3971
df-iin 3972
copk 4057
df-opk 4058
ax-nin 4078
ax-xp 4079
ax-cnv 4080
ax-1c 4081
ax-sset 4082
ax-si 4083
ax-ins2 4084
ax-ins3 4085
ax-typlower 4086
ax-sn 4087
cuni1 41331
c1c 4134 1c
cpw1 4135 1
df-1c 4136 1c
df-pw1 4137 1 1c
df-uni1 41381 1c
cxpk 4174 k
ccnvk 4175 k
cins2k 4176 Ins2k
cins3k 4177 Ins3k
cp6 4178 P6
cimak 4179 k
ccomk 4180 k
csik 4181 SIk
cimagek 4182 Imagek
cssetk 4183 SSetk
cidk 4184 k
df-xpk 4185 k
df-cnvk 4186 k
df-ins2k 4187 Ins2k
df-ins3k 4188 Ins3k
df-imak 4189 k
df-cok 4190 k Ins2k Ins3k kk
df-p6 4191 P6 k
df-sik 4192 SIk
df-ssetk 4193 SSetk
df-imagek 4194 Imagek k Ins2k SSetk Ins3k SSetk k k SIk k1 1 1c
df-idk 4195 k
cio 4337
df-iota 4339
cnnc 4373 Nn
c0c 4374 0c
cplc 4375
cfin 4376 Fin
df-0c 4377 0c
df-addc 4378
df-nnc 4379 Nn 0c 1c
df-fin 4380 Fin Nn
clefin 4431 <_fin
cltfin 4432 <fin
cncfin 4433 Ncfin
ctfin 4434 Tfin
cevenfin 4435 Evenfin
coddfin 4436 Oddfin
wsfin 4437 Sfin
cspfin 4438 Spfin
df-lefin 4439 <_fin Nn
df-ltfin 4440 <fin Nn 1c
df-ncfin 4441 Ncfin Nn
df-tfin 4442 Tfin Nn 1
df-evenfin 4443 Evenfin Nn
df-oddfin 4444 Oddfin Nn 1c
df-sfin 4445 Sfin Nn Nn 1
df-spfin 4446 Spfin Ncfin Sfin
cop 4561
cphi 4562 Phi
cproj1 4563 Proj1
cproj2 4564 Proj2
df-phi 4565 Phi Nn 1c
df-op 4566 Phi Phi 0c
df-proj1 4567 Proj1 Phi
df-proj2 4568 Proj2 Phi 0c
copab 4614
df-opab 4615
wbr 4631
df-br 4632
c1st 4709
cswap 4710 Swap
csset 4711 SSet
csi 4712 SI
ccom 4713
cima 4714
df-1st 4715
df-swap 4716 Swap
df-sset 4717 SSet
df-co 4718
df-ima 4719
df-si 4720 SI
cep 4754
cid 4755
df-eprel 4756
df-id 4759
cxp 4762
ccnv 4763
cdm 4764
crn 4765
cres 4766
wrel 4767
wfun 4768
wfn 4769
wf 4770
wf1 4771
wfo 4772
wf1o 4773
cfv 4774
wiso 4775
c2nd 4776
df-xp 4777
df-rel 4778
df-cnv 4779
df-rn 4780
df-dm 4781
df-res 4782
df-fun 4783
df-fn 4784
df-f 4785
df-f1 4786
df-fo 4787
df-f1o 4788
df-fv 4789
df-iso 4790
df-2nd 4791
co 5564
coprab 5565
df-ov 5566
df-oprab 5567
cmpt 5691
cmpt2 5692
df-mpt 5693
df-mpt2 5694
ctxp 5771
cpprod 5772 PProd
cfix 5773
cimage 5774 Image
ccup 5775 Cup
cdisj 5776 Disj
caddcfn 5777 AddC
cins2 5778 Ins2
cins3 5779 Ins3
cins4 5780 Ins4
csi3 5781 SI3
cfuns 5782 Funs
cfns 5783 Fns
ccross 5784 Cross
cpw1fn 5785 Pw1Fn
cfullfun 5786 FullFun
df-txp 5787
df-pprod 5788 PProd
df-fix 5789
df-cup 5790 Cup
df-disj 5791 Disj
df-addcfn 5792 AddC
df-ins2 5793 Ins2
df-ins3 5794 Ins3
df-image 5795 Image Ins2 SSet Ins3 SSet SI 1c
df-ins4 5796 Ins4
df-si3 5797 SI3 SI SI SI 1
df-funs 5798 Funs
df-fns 5799 Fns
df-cross 5800 Cross
df-pw1fn 5801 Pw1Fn 1c 1
df-fullfun 5802 FullFun
cclos1 5894 Clos1
df-clos1 5895 Clos1
ctrans 5908 Trans
cref 5909 Ref
cantisym 5910 Antisym
cpartial 5911 Po
cconnex 5912 Connex
cstrict 5913 Or
cfound 5914 Fr
cwe 5915 We
cext 5916 Ext
csym 5917 Sym
cer 5918 Er
df-trans 5919 Trans
df-ref 5920 Ref
df-antisym 5921 Antisym
df-partial 5922 Po Ref Trans Antisym
df-connex 5923 Connex
df-strict 5924 Or Po Connex
df-found 5925 Fr
df-we 5926 We Or Fr
df-ext 5927 Ext
df-sym 5928 Sym
df-er 5929 Er Sym Trans
cec 5965
cqs 5966
df-ec 5967
df-qs 5971
cmap 6019
cpm 6020
df-map 6021
df-pm 6022
cen 6048
df-en 6049
cncs 6108 NC
clec 6109 <_c
cltc 6110 <c
cnc 6111 Nc
cmuc 6112 ·c
ctc 6113 Tc
c2c 6114 2c
c3c 6115 3c
cce 6116c
ctcfn 6117 TcFn
df-ncs 6118 NC
df-lec 6119 <_c
df-ltc 6120 <c <_c
df-nc 6121 Nc
df-muc 6122 ·c NC NC
df-tc 6123 Tc NC Nc 1
df-2c 6124 2c Nc
df-3c 6125 3c Nc
df-ce 6126c NC NC 1 1
df-tcfn 6127 TcFn 1c Tc
cspac 6273 Spac
df-spac 6274 Spac NC Clos1 NC NC 2cc
  Copyright terms: Public domain W3C validator