Definition df-fn 5891

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6047, dffn3 6054, dffn4 6121, and dffn5 6241. (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 5883	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5882	. . 3 wff Fun 𝐴
5	1	cdm 5114	. . . 4 class dom 𝐴
6	5, 2	wceq 1483	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 384	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 196	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5918  fnsng  5938  fnprg  5947  fntpg  5948  fntp  5949  fncnv  5962  fneq1  5979  fneq2  5980  nffn  5987  fnfun  5988  fndm  5990  fnun  5997  fnco  5999  fnssresb  6003  fnres  6007  fnresi  6008  fn0  6011  mptfnf  6015  fnopabg  6017  sbcfng  6042  fdmrn  6064  fcoi1  6078  f00  6087  f1cnvcnv  6109  fores  6124  dff1o4  6145  foimacnv  6154  funfv  6265  fvimacnvALT  6336  respreima  6344  dff3  6372  fpr  6421  fnsnb  6432  fnprb  6472  fnex  6481  fliftf  6565  fnoprabg  6761  fun11iun  7126  f1oweALT  7152  curry1  7269  curry2  7272  tposfn2  7374  wfrlem13  7427  wfr1  7433  tfrlem10  7483  tfr1  7493  frfnom  7530  undifixp  7944  sbthlem9  8078  fodomr  8111  rankf  8657  cardf2  8769  axdc3lem2  9273  nqerf  9752  axaddf  9966  axmulf  9967  uzrdgfni  12757  hashkf  13119  shftfn  13813  imasaddfnlem  16188  imasvscafn  16197  fntopon  20728  cnextf  21870  ftc1cn  23806  grporn  27375  ffsrn  29504  measdivcstOLD  30287  bnj145OLD  30795  bnj1422  30908  nofnbday  31805  elno2  31807  scutf  31919  fnsingle  32026  fnimage  32036  imageval  32037  dfrecs2  32057  dfrdg4  32058  ftc1cnnc  33484  fnresfnco  41206  funcoressn  41207  afvco2  41256