Definition df-fn 4925

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-fn	⊢ (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

Detailed syntax breakdown of Definition df-fn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wfn 4917	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 4916	. . 3 wff Fun 𝐴
5	1	cdm 4363	. . . 4 class dom 𝐴
6	5, 2	wceq 1284	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 102	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 103	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  4951  fnsng  4967  fnprg  4974  fntpg  4975  fntp  4976  fncnv  4985  fneq1  5007  fneq2  5008  nffn  5015  fnfun  5016  fndm  5018  fnun  5025  fnco  5027  fnssresb  5031  fnres  5035  fnresi  5036  fn0  5038  fnopabg  5042  sbcfng  5064  fcoi1  5090  f00  5101  f1cnvcnv  5120  fores  5135  dff1o4  5154  foimacnv  5164  fun11iun  5167  funfvdm  5257  respreima  5316  fpr  5366  fnex  5404  fliftf  5459  fnoprabg  5622  tposfn2  5904  tfrlemibfn  5965  tfri1d  5972  frecuzrdgfn  9414  shftfn  9712