![]() |
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 5480 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5384 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5230 ⟶wf 5231 –1-1-onto→wf1o 5234 |
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 5239 df-f1 5240 df-f1o 5242 |
This theorem is referenced by: f1ofun 5482 f1odm 5484 isocnv2 5834 isoini 5840 isoselem 5842 bren 6774 en1 6826 xpen 6874 phplem4 6884 phplem4on 6896 dif1en 6908 fiintim 6958 supisolem 7038 ordiso2 7065 inresflem 7090 eldju 7098 caseinl 7121 caseinr 7122 enomnilem 7167 enmkvlem 7190 enwomnilem 7198 iseqf1olemnab 10521 hashfacen 10851 fprodssdc 11633 phimullem 12260 |
Copyright terms: Public domain | W3C validator |