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 5335 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5242 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5088 ⟶wf 5089 –1-1-onto→wf1o 5092 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f 5097 df-f1 5098 df-f1o 5100 |
This theorem is referenced by: f1ofun 5337 f1odm 5339 isocnv2 5681 isoini 5687 isoselem 5689 bren 6609 en1 6661 xpen 6707 phplem4 6717 phplem4on 6729 dif1en 6741 fiintim 6785 supisolem 6863 ordiso2 6888 inresflem 6913 eldju 6921 caseinl 6944 caseinr 6945 enomnilem 6978 iseqf1olemnab 10229 hashfacen 10547 phimullem 11828 |
Copyright terms: Public domain | W3C validator |