Definition df-fn 5383

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 5375	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5374	. . 3 wff Fun 𝐴
5	1	cdm 4776	. . . 4 class dom 𝐴
6	5, 2	wceq 1402	. . 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 used by:  funfn  5410  fnsng  5431  fnprg  5439  fntpg  5440  fntp  5441  fncnv  5450  fneq1  5472  fneq2  5473  nffn  5480  fnfun  5481  fndm  5483  fnun  5492  fnco  5494  fnssresb  5498  fnres  5503  fnresi  5504  fn0  5506  fnopabg  5510  sbcfng  5534  fcoi1  5575  f00  5587  f1cnvcnv  5612  fores  5628  dff1o4  5650  foimacnv  5660  fun11iun  5663  funfvdm  5769  respreima  5839  fpr  5900  fnex  5940  fliftf  6008  fdmrn  6037  fnoprabg  6192  tposfn2  6541  tfrlemibfn  6603  tfri1d  6610  tfr1onlembfn  6619  tfri1dALT  6626  tfrcllembfn  6632  sbthlemi9  7287  caseinl  7437  caseinr  7438  ctssdccl  7457  exmidfodomrlemim  7559  axaddf  8241  axmulf  8242  frecuzrdgtcl  10870  frecuzrdgtclt  10879  shftfn  11611  imasaddfnlemg  13694  fntopon  15250