Theorem fof 5418

Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
fof	⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem fof

Step	Hyp	Ref	Expression
1		eqimss 3201	. . 3 ⊢ (ran 𝐹 = 𝐵 → ran 𝐹 ⊆ 𝐵)
2	1	anim2i 340	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
3		df-fo 5202	. 2 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4		df-f 5200	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5	2, 3, 4	3imtr4i 200	1 ⊢ (𝐹:𝐴–onto→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348   ⊆ wss 3121  ran crn 4610   Fn wfn 5191  ⟶wf 5192  –onto→wfo 5194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134  df-f 5200  df-fo 5202

This theorem is referenced by:  fofun  5419  fofn  5420  dffo2  5422  foima  5423  resdif  5462  ffoss  5472  fconstfvm  5711  cocan2  5764  foeqcnvco  5766  fornex  6091  algrflem  6205  algrflemg  6206  tposf2  6244  mapsn  6664  ssdomg  6752  fopwdom  6810  fidcenumlemrks  6926  fidcenumlemr  6928  ctmlemr  7081  ctm  7082  ctssdclemn0  7083  ctssdccl  7084  ctssdc  7086  enumctlemm  7087  enumct  7088  fodjuomnilemdc  7116  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  suplocexprlemdisj  7669  suplocexprlemub  7672  focdmex  10708  ennnfonelemdc  12341  ennnfonelemg  12345  ennnfonelemp1  12348  ennnfonelemhdmp1  12351  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ennnfonelemex  12356  ennnfonelemhom  12357  ctinfomlemom  12369  ctinf  12372  ctiunctlemudc  12379  ctiunctlemf  12380  omctfn  12385  dvrecap  13392  subctctexmid  13956  pw1nct  13958