Definition df-fn 6040

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6196, dffn3 6203, dffn4 6270, and dffn5 6391. (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 6032	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6031	. . 3 wff Fun 𝐴
5	1	cdm 5254	. . . 4 class dom 𝐴
6	5, 2	wceq 1620	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 383	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 196	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6067  fnsng  6087  fnprg  6096  fntpg  6097  fntp  6098  fncnv  6111  fneq1  6128  fneq2  6129  nffn  6136  fnfun  6137  fndm  6139  fnun  6146  fnco  6148  fnssresb  6152  fnres  6156  fnresi  6157  fn0  6160  mptfnf  6164  fnopabg  6166  sbcfng  6191  fdmrn  6213  fcoi1  6227  f00  6236  f1cnvcnv  6258  fores  6273  dff1o4  6294  foimacnv  6303  funfv  6415  fvimacnvALT  6487  respreima  6495  dff3  6523  fpr  6572  fnsnb  6584  fnprb  6624  fnex  6633  fliftf  6716  fnoprabg  6914  fun11iun  7279  f1oweALT  7305  curry1  7425  curry2  7428  tposfn2  7531  wfrlem13  7584  wfr1  7590  tfrlem10  7640  tfr1  7650  frfnom  7687  undifixp  8098  sbthlem9  8231  fodomr  8264  rankf  8818  cardf2  8930  axdc3lem2  9436  nqerf  9915  axaddf  10129  axmulf  10130  uzrdgfni  12922  hashkf  13284  shftfn  13983  imasaddfnlem  16361  imasvscafn  16370  fntopon  20901  cnextf  22042  ftc1cn  23976  grporn  27655  ffsrn  29784  measdivcstOLD  30567  bnj1422  31186  nofnbday  32082  elno2  32084  scutf  32196  fnsingle  32303  fnimage  32313  imageval  32314  dfrecs2  32334  dfrdg4  32335  ftc1cnnc  33766  fnresfnco  41681  funcoressn  41682  afvco2  41731