Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 Rel wrel 5672
Fun wfun 6528 Fn wfn 6529 |
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 396
df-fun 6536 df-fn 6537 |
This theorem is referenced by: fnbr
6648 fnunres1
6652 fnresdm
6660 fn0
6672 frel
6713 fcoi2
6757 f1rel
6781 f1ocnv
6836 dffn5
6941 feqmptdf
6953 fnsnfvOLD
6962 fconst5
7200 fnex
7211 fnexALT
7931 tz7.48-2
8438 resfnfinfin
9329 zorn2lem4
10491 imasvscafn
17488 2oppchomf
17675 opprabs
33091 bnj66
34389 tfsconcatb0
42643 tfsconcat0i
42644 tfsconcat0b
42645 tfsconcat00
42646 fnresdmss
44412 dfafn5a
46413 |