Definition df-fn 5357

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 5349	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5348	. . 3 wff Fun 𝐴
5	1	cdm 4751	. . . 4 class dom 𝐴
6	5, 2	wceq 1398	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 104	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 105	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5384  fnsng  5405  fnprg  5413  fntpg  5414  fntp  5415  fncnv  5424  fneq1  5446  fneq2  5447  nffn  5454  fnfun  5455  fndm  5457  fnun  5466  fnco  5468  fnssresb  5472  fnres  5477  fnresi  5478  fn0  5480  fnopabg  5484  sbcfng  5508  fcoi1  5549  f00  5561  f1cnvcnv  5586  fores  5602  dff1o4  5624  foimacnv  5634  fun11iun  5637  funfvdm  5742  respreima  5807  fpr  5868  fnex  5908  fliftf  5974  fnoprabg  6156  tposfn2  6499  tfrlemibfn  6561  tfri1d  6568  tfr1onlembfn  6577  tfri1dALT  6584  tfrcllembfn  6590  sbthlemi9  7237  caseinl  7384  caseinr  7385  ctssdccl  7404  exmidfodomrlemim  7506  axaddf  8185  axmulf  8186  frecuzrdgtcl  10778  frecuzrdgtclt  10787  shftfn  11513  imasaddfnlemg  13544  fntopon  14906