Change to Unicode version
|
|
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-1 5 |  |
| ax-2 6 |  |
| ax-3 7 | |
| ax-mp 8 |   |
| wb 176 |  |
| df-bi 177 |
|
| wo 357 |  |
| wa 358 | ![](wedge.gif "/\"){kind=small} |
| df-or 359 |
|
| df-an 360 |
|
| w3o 933 | |
| w3a 934 | |
| df-3or 935 | |
| df-3an 936 | |
| wnan 1287 | ![](barwedge.gif "-/\"){kind=small} |
| 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 | 
![].](_drbrack.gif "]."){kind=small} |
| df-sbc 3047 | |
| csb 3136 |   |
| df-csb 3137 |
|
| cnin 3204 |
&ncap |
| ccompl 3205 | ∼ |
| cdif 3206 |
![](setminus.gif "\"){kind=small} |
| 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 |