Colors of
variables: wff set class |
Syntax hints:
→ wi 4 Fun wfun 5210
Fn wfn 5211 –1-1-onto→wf1o 5215 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 |
This theorem depends on definitions:
df-bi 117 df-fn 5219 df-f 5220 df-f1 5221 df-f1o 5223 |
This theorem is referenced by: f1orel
5464 f1oresrab
5681 isose
5821 f1opw
6077 xpcomco
6825 fiintim
6927 f1dmvrnfibi
6942 caseinl
7089 caseinr
7090 ctssdccl
7109 ctssdclemr
7110 fihasheqf1oi
10766 fisumss
11399 ennnfonelemex
12414 ennnfonelemf1
12418 hmeontr
13783 |