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

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	⊢ ( 𝐴 Fn 𝐵 ↔ ( Fun 𝐴 ∧ dom 𝐴 = 𝐵 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	wfn	⊢ 𝐴 Fn 𝐵
3	0	wfun	⊢ Fun 𝐴
4	0	cdm	⊢ dom 𝐴
5	4 1	wceq	⊢ dom 𝐴 = 𝐵
6	3 5	wa	⊢ ( Fun 𝐴 ∧ dom 𝐴 = 𝐵 )
7	2 6	wb	⊢ ( 𝐴 Fn 𝐵 ↔ ( Fun 𝐴 ∧ dom 𝐴 = 𝐵 ) )