Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 Rel wrel 5639
Fun wfun 6491 Fn wfn 6492 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-fun 6499 df-fn 6500 |
This theorem is referenced by: fnbr
6611 fnresdm
6621 fn0
6633 frel
6674 fcoi2
6718 f1rel
6742 f1ocnv
6797 dffn5
6902 feqmptdf
6913 fnsnfvOLD
6922 fconst5
7156 fnex
7168 fnexALT
7884 tz7.48-2
8389 resfnfinfin
9277 zorn2lem4
10436 imasvscafn
17420 2oppchomf
17607 fnunres1
31527 bnj66
33475 fnresdmss
43392 dfafn5a
45399 |