Colors of
variables: wff set class |
Syntax hints:
→ wi 4 Fun wfun 5202
Fn wfn 5203 –1-1-onto→wf1o 5207 |
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 5211 df-f 5212 df-f1 5213 df-f1o 5215 |
This theorem is referenced by: f1orel
5456 f1oresrab
5673 isose
5812 f1opw
6068 xpcomco
6816 fiintim
6918 f1dmvrnfibi
6933 caseinl
7080 caseinr
7081 ctssdccl
7100 ctssdclemr
7101 fihasheqf1oi
10734 fisumss
11367 ennnfonelemex
12381 ennnfonelemf1
12385 hmeontr
13306 |