Metamath Proof Explorer


Definition df-fn

Description: Define a function with domain. Definition 6.15(1) of TakeutiZaring p. 27. For alternate definitions, see dffn2 , dffn3 , dffn4 , and dffn5 . (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion df-fn A Fn B Fun A dom A = B

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 0 1 wfn wff A Fn B
3 0 wfun wff Fun A
4 0 cdm class dom A
5 4 1 wceq wff dom A = B
6 3 5 wa wff Fun A dom A = B
7 2 6 wb wff A Fn B Fun A dom A = B