This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-f

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of TakeutiZaring p. 27. F : A --> B can be read as " F is a function from A to B ". For alternate definitions, see dff2 , dff3 , and dff4 . (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	1 2 0	wf	⊢ 𝐹 : 𝐴 ⟶ 𝐵
4	0 1	wfn	⊢ 𝐹 Fn 𝐴
5	0	crn	⊢ ran 𝐹
6	5 2	wss	⊢ ran 𝐹 ⊆ 𝐵
7	4 6	wa	⊢ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 )
8	3 7	wb	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )