New Foundations Explorer |
This is the GIF version. Change to Unicode version |
Ref | Expression (see link for any distinct variable requirements) |
wn 3 | |
wi 4 | |
ax-mp 5 | |
ax-1 6 | |
ax-2 7 | |
ax-3 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 | |
df-nf 1545 | |
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 | |
df-nfc 2478 | |
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 4133 | ⋃1 |
c1c 4134 | 1c |
cpw1 4135 | 1 |
df-1c 4136 | 1c |
df-pw1 4137 | 1 1c |
df-uni1 4138 | ⋃1 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 | Sk |
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 | Sk |
df-imagek 4194 | Imagek k Ins2k Sk Ins3k Sk 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 4432 | fin |
cltfin 4433 | fin |
cncfin 4434 | Ncfin |
ctfin 4435 | Tfin |
cevenfin 4436 | Evenfin |
coddfin 4437 | Oddfin |
wsfin 4438 | Sfin |
cspfin 4439 | Spfin |
df-lefin 4440 | fin Nn |
df-ltfin 4441 | fin Nn 1c |
df-ncfin 4442 | Ncfin Nn |
df-tfin 4443 | Tfin Nn 1 |
df-evenfin 4444 | Evenfin Nn |
df-oddfin 4445 | Oddfin Nn 1c |
df-sfin 4446 | Sfin Nn Nn 1 |
df-spfin 4447 | 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 4622 | |
df-opab 4623 | |
wbr 4639 | |
df-br 4640 | |
c1st 4717 | |
cswap 4718 | Swap |
csset 4719 | S |
csi 4720 | SI |
ccom 4721 | |
cima 4722 | |
df-1st 4723 | |
df-swap 4724 | Swap |
df-sset 4725 | S |
df-co 4726 | |
df-ima 4727 | |
df-si 4728 | SI |
cep 4762 | |
cid 4763 | |
df-eprel 4764 | |
df-id 4767 | |
cxp 4770 | |
ccnv 4771 | |
cdm 4772 | |
crn 4773 | |
cres 4774 | |
wfun 4775 | |
wfn 4776 | |
wf 4777 | |
wf1 4778 | |
wfo 4779 | |
wf1o 4780 | |
cfv 4781 | |
wiso 4782 | |
c2nd 4783 | |
df-xp 4784 | |
df-cnv 4785 | |
df-rn 4786 | |
df-dm 4787 | |
df-res 4788 | |
df-fun 4789 | |
df-fn 4790 | |
df-f 4791 | |
df-f1 4792 | |
df-fo 4793 | |
df-f1o 4794 | |
df-fv 4795 | |
df-iso 4796 | |
df-2nd 4797 | |
co 5525 | |
df-ov 5526 | |
coprab 5527 | |
df-oprab 5528 | |
cmpt 5651 | |
df-mpt 5652 | |
cmpt2 5653 | |
df-mpt2 5654 | |
ctxp 5735 | |
df-txp 5736 | |
cpprod 5737 | PProd |
df-pprod 5738 | PProd |
cfix 5739 | |
df-fix 5740 | |
ccup 5741 | Cup |
df-cup 5742 | Cup |
cdisj 5743 | Disj |
df-disj 5744 | Disj |
caddcfn 5745 | AddC |
df-addcfn 5746 | AddC |
ccompose 5747 | Compose |
df-compose 5748 | Compose |
cins2 5749 | Ins2 |
df-ins2 5750 | Ins2 |
cins3 5751 | Ins3 |
df-ins3 5752 | Ins3 |
cimage 5753 | Image |
df-image 5754 | Image ∼ Ins2 S Ins3 S SI 1c |
cins4 5755 | Ins4 |
df-ins4 5756 | Ins4 |
csi3 5757 | SI3 |
df-si3 5758 | SI3 SI SI SI 1 |
cfuns 5759 | Funs |
df-funs 5760 | Funs |
cfns 5761 | Fns |
df-fns 5762 | Fns |
ccross 5763 | Cross |
df-cross 5764 | Cross |
cpw1fn 5765 | Pw1Fn |
df-pw1fn 5766 | Pw1Fn 1c 1 |
cfullfun 5767 | FullFun |
df-fullfun 5768 | FullFun ∼ ∼ ∼ |
cdomfn 5769 | Dom |
df-domfn 5770 | Dom |
cranfn 5771 | Ran |
df-ranfn 5772 | Ran |
cclos1 5872 | Clos1 |
df-clos1 5873 | Clos1 |
ctrans 5888 | Trans |
cref 5889 | Ref |
cantisym 5890 | Antisym |
cpartial 5891 | Po |
cconnex 5892 | Connex |
cstrict 5893 | Or |
cfound 5894 | Fr |
cwe 5895 | We |
cext 5896 | Ext |
csym 5897 | Sym |
cer 5898 | Er |
df-trans 5899 | Trans |
df-ref 5900 | Ref |
df-antisym 5901 | Antisym |
df-partial 5902 | Po Ref Trans Antisym |
df-connex 5903 | Connex |
df-strict 5904 | Or Po Connex |
df-found 5905 | Fr |
df-we 5906 | We Or Fr |
df-ext 5907 | Ext |
df-sym 5908 | Sym |
df-er 5909 | Er Sym Trans |
cec 5945 | |
cqs 5946 | |
df-ec 5947 | |
df-qs 5951 | |
cmap 5999 | |
cpm 6000 | |
df-map 6001 | |
df-pm 6002 | |
cen 6028 | |
df-en 6029 | |
cncs 6088 | NC |
clec 6089 | c |
cltc 6090 | c |
cnc 6091 | Nc |
cmuc 6092 | ·c |
ctc 6093 | Tc |
c2c 6094 | 2c |
c3c 6095 | 3c |
cce 6096 | ↑c |
ctcfn 6097 | TcFn |
df-ncs 6098 | NC |
df-lec 6099 | c |
df-ltc 6100 | c c |
df-nc 6101 | Nc |
df-muc 6102 | ·c NC NC |
df-tc 6103 | Tc NC Nc 1 |
df-2c 6104 | 2c Nc |
df-3c 6105 | 3c Nc |
df-ce 6106 | ↑c NC NC 1 1 |
df-tcfn 6107 | TcFn 1c Tc |
cspac 6273 | Spac |
df-spac 6274 | Spac NC Clos1 NC NC 2c ↑c |
cfrec 6309 | FRec |
df-frec 6310 | FRec Clos1 0c PProd 1c |
ccan 6323 | Can |
df-can 6324 | Can 1 |
cscan 6325 | SCan |
df-scan 6326 | SCan |
Copyright terms: Public domain | W3C validator |