![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > f1ofn | GIF version |
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.) |
Ref | Expression |
---|---|
f1ofn | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1of 5456 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5360 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5206 ⟶wf 5207 –1-1-onto→wf1o 5210 |
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-f 5215 df-f1 5216 df-f1o 5218 |
This theorem is referenced by: f1ofun 5458 f1odm 5460 isocnv2 5806 isoini 5812 isoselem 5814 bren 6740 en1 6792 xpen 6838 phplem4 6848 phplem4on 6860 dif1en 6872 fiintim 6921 supisolem 7000 ordiso2 7027 inresflem 7052 eldju 7060 caseinl 7083 caseinr 7084 enomnilem 7129 enmkvlem 7152 enwomnilem 7160 iseqf1olemnab 10461 hashfacen 10787 fprodssdc 11569 phimullem 12195 |
Copyright terms: Public domain | W3C validator |