Definition df-fn 6436

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6602, dffn3 6613, dffn4 6694, and dffn5 6828. (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 6428	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6427	. . 3 wff Fun 𝐴
5	1	cdm 5589	. . . 4 class dom 𝐴
6	5, 2	wceq 1539	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 396	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 205	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6464  fnsng  6486  fnprg  6493  fntpg  6494  fntp  6495  fncnv  6507  fneq1  6524  fneq2  6525  nffn  6532  fnfun  6533  fndm  6536  fnun  6545  fncoOLD  6550  fnssresb  6554  fnres  6559  idfn  6560  fnresiOLD  6562  fn0  6564  mptfnf  6568  fnopabg  6570  sbcfng  6597  fdmrn  6632  fcoi1  6648  f00  6656  f1cnvcnv  6680  fores  6698  dff1o4  6724  foimacnv  6733  funfv  6855  fvimacnvALT  6934  respreima  6943  dff3  6976  fpr  7026  fnsnb  7038  fnprb  7084  fnex  7093  fliftf  7186  fnoprabg  7397  fiun  7785  f1iun  7786  f1oweALT  7815  curry1  7944  curry2  7947  tposfn2  8064  frrlem11  8112  frrlem12  8113  fpr1  8119  wfrlem13OLD  8152  wfr1OLD  8158  tfrlem10  8218  tfr1  8228  frfnom  8266  undifixp  8722  sbthlem9  8878  fodomr  8915  frr1  9517  rankf  9552  cardf2  9701  axdc3lem2  10207  nqerf  10686  axaddf  10901  axmulf  10902  uzrdgfni  13678  hashkf  14046  shftfn  14784  imasaddfnlem  17239  imasvscafn  17248  fntopon  22073  cnextf  23217  ftc1cn  25207  grporn  28883  ffsrn  31064  measdivcstALTV  32193  bnj1422  32817  satff  33372  nofnbday  33855  scutf  34006  fnsingle  34221  fnimage  34231  imageval  34232  dfrecs2  34252  dfrdg4  34253  bj-isrvec  35465  ftc1cnnc  35849  fnresfnco  44535  funcoressn  44536  afvco2  44668