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 2477 | |
df-nfc 2479 | |
wne 2517 | |
wnel 2518 | |
df-ne 2519 |
|
df-nel 2520 | |
wral 2615 |
|
wrex 2616 |
|
wreu 2617 |
|
wrmo 2618 |
|
crab 2619 | |
df-ral 2620 |
|
df-rex 2621 |
|
df-reu 2622 |
|
df-rmo 2623 |
|
df-rab 2624 |
|
cvv 2860 | |
df-v 2862 |
|
wsbc 3047 |
|
df-sbc 3048 | |
csb 3137 | |
df-csb 3138 |
|
cnin 3205 |
&ncap |
ccompl 3206 | ∼ |
cdif 3207 |
|
cun 3208 |
|
cin 3209 |
|
csymdif 3210 |
|
df-nin 3212 | &ncap
|
df-compl 3213 | ∼
&ncap |
df-in 3214 |
∼ &ncap |
df-un 3215 |
∼ &ncap ∼ |
df-dif 3216 |
∼ |
df-symdif 3217 |
|
wss 3258 | |
wpss 3259 | |
df-ss 3260 |
|
df-pss 3262 |
|
c0 3551 | |
df-nul 3552 | |
cif 3663 | |
df-if 3664 |
|
cpw 3723 | |
df-pw 3725 |
|
csn 3738 | |
cpr 3739 | |
ctp 3740 | |
df-sn 3742 |
|
df-pr 3743 | |
df-tp 3744 |
|
cuni 3892 | |
df-uni 3893 |
|
cint 3927 | |
df-int 3928 | |
ciun 3970 | |
ciin 3971 | |
df-iun 3972 |
|
df-iin 3973 |
|
copk 4058 |
|
df-opk 4059 | |
ax-nin 4079 | |
ax-xp 4080 | |
ax-cnv 4081 | |
ax-1c 4082 | |
ax-sset 4083 |
|
ax-si 4084 | |
ax-ins2 4085 |
|
ax-ins3 4086 |
|
ax-typlower 4087 | |
ax-sn 4088 | |
cuni1 4134 | ⋃1 |
c1c 4135 | 1c |
cpw1 4136 | 1 |
df-1c 4137 | 1c
|
df-pw1 4138 | 1
1c |
df-uni1 4139 | ⋃1 1c |
cxpk 4175 |
k
|
ccnvk 4176 | k |
cins2k 4177 | Ins2k |
cins3k 4178 | Ins3k |
cp6 4179 | P6
|
cimak 4180 | k |
ccomk 4181 |
k
|
csik 4182 | SIk |
cimagek 4183 | Imagek |
cssetk 4184 | Sk |
cidk 4185 | k |
df-xpk 4186 | k
|
df-cnvk 4187 | k
|
df-ins2k 4188 | Ins2k
|
df-ins3k 4189 | Ins3k
|
df-imak 4190 | k
|
df-cok 4191 | k Ins2k Ins3k
kk |
df-p6 4192 | P6
k |
df-sik 4193 | SIk
|
df-ssetk 4194 | Sk
|
df-imagek 4195 | Imagek k Ins2k Sk Ins3k Sk k k SIk k1 1 1c |
df-idk 4196 | k |
cio 4338 | |
df-iota 4340 |
|
cnnc 4374 | Nn |
c0c 4375 | 0c |
cplc 4376 |
|
cfin 4377 | Fin |
df-0c 4378 | 0c |
df-addc 4379 |
|
df-nnc 4380 | Nn 0c
1c
|
df-fin 4381 | Fin Nn |
clefin 4433 | fin |
cltfin 4434 | fin |
cncfin 4435 | Ncfin |
ctfin 4436 | Tfin |
cevenfin 4437 | Evenfin |
coddfin 4438 | Oddfin |
wsfin 4439 | Sfin
|
cspfin 4440 | Spfin |
df-lefin 4441 | fin Nn |
df-ltfin 4442 | fin
Nn
1c |
df-ncfin 4443 | Ncfin
Nn |
df-tfin 4444 | Tfin
Nn
1 |
df-evenfin 4445 | Evenfin
Nn |
df-oddfin 4446 | Oddfin
Nn 1c |
df-sfin 4447 | Sfin
Nn Nn 1
|
df-spfin 4448 | Spfin
Ncfin
Sfin |
cop 4562 |
|
cphi 4563 | Phi
|
cproj1 4564 | Proj1 |
cproj2 4565 | Proj2 |
df-phi 4566 | Phi
Nn 1c |
df-op 4567 |
Phi
Phi 0c |
df-proj1 4568 | Proj1
Phi |
df-proj2 4569 | Proj2
Phi 0c |
copab 4623 | |
df-opab 4624 |
|
wbr 4640 | |
df-br 4641 | |
c1st 4718 | |
cswap 4719 | Swap
|
csset 4720 | S
|
csi 4721 | SI
|
ccom 4722 |
|
cima 4723 | |
df-1st 4724 |
|
df-swap 4725 | Swap |
df-sset 4726 | S
|
df-co 4727 |
|
df-ima 4728 |
|
df-si 4729 | SI |
cep 4763 | |
cid 4764 | |
df-eprel 4765 |
|
df-id 4768 |
|
cxp 4771 |
|
ccnv 4772 | |
cdm 4773 | |
crn 4774 | |
cres 4775 |
|
wfun 4776 | |
wfn 4777 | |
wf 4778 | |
wf1 4779 | |
wfo 4780 | |
wf1o 4781 | |
cfv 4782 | |
wiso 4783 | |
c2nd 4784 | |
df-xp 4785 |
|
df-cnv 4786 |
|
df-rn 4787 | |
df-dm 4788 | |
df-res 4789 |
|
df-fun 4790 | |
df-fn 4791 |
|
df-f 4792 | |
df-f1 4793 | |
df-fo 4794 | |
df-f1o 4795 | |
df-fv 4796 | |
df-iso 4797 |
|
df-2nd 4798 |
|
co 5526 | |
df-ov 5527 | |
coprab 5528 | |
df-oprab 5529 | |
cmpt 5652 |
|
df-mpt 5653 |
|
cmpt2 5654 |
|
df-mpt2 5655 |
|
ctxp 5736 |
|
df-txp 5737 |
|
cpprod 5738 | PProd |
df-pprod 5739 | PProd
|
cfix 5740 | |
df-fix 5741 | |
ccup 5742 | Cup |
df-cup 5743 | Cup
|
cdisj 5744 | Disj |
df-disj 5745 | Disj
|
caddcfn 5746 | AddC |
df-addcfn 5747 | AddC
|
ccompose 5748 | Compose |
df-compose 5749 | Compose
|
cins2 5750 | Ins2
|
df-ins2 5751 | Ins2 |
cins3 5752 | Ins3
|
df-ins3 5753 | Ins3
|
cimage 5754 | Image |
df-image 5755 | Image
∼ Ins2 S Ins3 S SI 1c |
cins4 5756 | Ins4
|
df-ins4 5757 | Ins4 |
csi3 5758 | SI3 |
df-si3 5759 | SI3 SI
SI SI 1 |
cfuns 5760 | Funs |
df-funs 5761 | Funs
|
cfns 5762 | Fns |
df-fns 5763 | Fns |
ccross 5764 | Cross |
df-cross 5765 | Cross
|
cpw1fn 5766 | Pw1Fn |
df-pw1fn 5767 | Pw1Fn
1c 1 |
cfullfun 5768 | FullFun |
df-fullfun 5769 | FullFun
∼ ∼
∼ |
cdomfn 5770 | Dom |
df-domfn 5771 | Dom |
cranfn 5772 | Ran |
df-ranfn 5773 | Ran |
cclos1 5873 | Clos1 |
df-clos1 5874 | Clos1
|
ctrans 5889 | Trans |
cref 5890 | Ref |
cantisym 5891 | Antisym |
cpartial 5892 | Po |
cconnex 5893 | Connex |
cstrict 5894 | Or |
cfound 5895 | Fr |
cwe 5896 | We |
cext 5897 | Ext |
csym 5898 | Sym |
cer 5899 | Er |
df-trans 5900 | Trans
|
df-ref 5901 | Ref
|
df-antisym 5902 | Antisym
|
df-partial 5903 | Po Ref Trans Antisym |
df-connex 5904 | Connex
|
df-strict 5905 | Or Po Connex |
df-found 5906 | Fr
|
df-we 5907 | We Or Fr |
df-ext 5908 | Ext
|
df-sym 5909 | Sym
|
df-er 5910 | Er Sym Trans |
cec 5946 | |
cqs 5947 | |
df-ec 5948 | |
df-qs 5952 |
|
cmap 6000 | |
cpm 6001 | |
df-map 6002 |
|
df-pm 6003 |
|
cen 6029 | |
df-en 6030 | |
cncs 6089 | NC |
clec 6090 | c |
cltc 6091 | c |
cnc 6092 | Nc
|
cmuc 6093 |
·c |
ctc 6094 | Tc |
c2c 6095 | 2c |
c3c 6096 | 3c |
cce 6097 | ↑c |
ctcfn 6098 | TcFn |
df-ncs 6099 | NC |
df-lec 6100 | c
|
df-ltc 6101 | c c |
df-nc 6102 | Nc |
df-muc 6103 | ·c
NC NC
|
df-tc 6104 | Tc
NC Nc 1 |
df-2c 6105 | 2c Nc |
df-3c 6106 | 3c Nc |
df-ce 6107 | ↑c NC NC 1
1 |
df-tcfn 6108 | TcFn 1c Tc |
cspac 6274 | Spac |
df-spac 6275 | Spac
NC Clos1 NC NC 2c ↑c
|
cfrec 6310 | FRec
|
df-frec 6311 | FRec Clos1 0c PProd
1c |
ccan 6324 | Can |
df-can 6325 | Can
1 |
cscan 6326 | SCan |
df-scan 6327 | SCan
|