Definition df-fn 5360

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 5352	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5351	. . 3 wff Fun 𝐴
5	1	cdm 4754	. . . 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  5387  fnsng  5408  fnprg  5416  fntpg  5417  fntp  5418  fncnv  5427  fneq1  5449  fneq2  5450  nffn  5457  fnfun  5458  fndm  5460  fnun  5469  fnco  5471  fnssresb  5475  fnres  5480  fnresi  5481  fn0  5483  fnopabg  5487  sbcfng  5511  fcoi1  5552  f00  5564  f1cnvcnv  5589  fores  5605  dff1o4  5627  foimacnv  5637  fun11iun  5640  funfvdm  5745  respreima  5810  fpr  5871  fnex  5911  fliftf  5978  fdmrn  6007  fnoprabg  6162  tposfn2  6510  tfrlemibfn  6572  tfri1d  6579  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  sbthlemi9  7248  caseinl  7395  caseinr  7396  ctssdccl  7415  exmidfodomrlemim  7517  axaddf  8199  axmulf  8200  frecuzrdgtcl  10798  frecuzrdgtclt  10807  shftfn  11534  imasaddfnlemg  13578  fntopon  15015