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 ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF class F
1 cA class A
2 cB class B
3 1 2 0 wf wff F : A ⟶ B
4 0 1 wfn wff F Fn A
5 0 crn class ran ⁡ F
6 5 2 wss wff ran ⁡ F ⊆ B
7 4 6 wa wff F Fn A ∧ ran ⁡ F ⊆ B
8 3 7 wb wff F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B