![]() |
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 5266 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5174 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5023 ⟶wf 5024 –1-1-onto→wf1o 5027 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f 5032 df-f1 5033 df-f1o 5035 |
This theorem is referenced by: f1ofun 5268 f1odm 5270 isocnv2 5605 isoini 5611 isoselem 5613 bren 6518 en1 6570 xpen 6615 phplem4 6625 phplem4on 6637 dif1en 6649 fiintim 6693 supisolem 6757 ordiso2 6782 inresflem 6806 eldju 6813 caseinl 6836 enomnilem 6855 iseqf1olemnab 9978 hashfacen 10302 phimullem 11540 |
Copyright terms: Public domain | W3C validator |