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 
 |-  A
1 cB 
 |-  B
2 0 1 wfn 
 |-  A Fn B
3 0 wfun 
 |-  Fun A
4 0 cdm 
 |-  dom A
5 4 1 wceq 
 |-  dom A = B
6 3 5 wa 
 |-  ( Fun A /\ dom A = B )
7 2 6 wb 
 |-  ( A Fn B <-> ( Fun A /\ dom A = B ) )