Definition df-fn 6483

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6654, dffn3 6665, dffn4 6746, and dffn5 6885. (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 6475	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6474	. . 3 wff Fun 𝐴
5	1	cdm 5621	. . . 4 class dom 𝐴
6	5, 2	wceq 1540	. . 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  6515  fnsng  6537  fnprg  6544  fntpg  6545  fntp  6546  fncnv  6558  fneq1  6577  fneq2  6578  nffn  6585  fnfun  6586  fndm  6589  fnun  6598  fncoOLD  6603  fnssresb  6607  fnres  6612  idfn  6613  fn0  6616  mptfnf  6620  fnopabg  6622  sbcfng  6649  fdmrn  6684  fcoi1  6700  f00  6708  f1cnvcnv  6732  fores  6750  dff1o4  6776  foimacnv  6785  funfv  6912  fvimacnvALT  6991  respreima  7000  dff3  7033  fpr  7083  fnsnb  7095  fnprb  7141  fnex  7150  fliftf  7243  fnoprabg  7460  fiun  7854  f1iun  7855  f1oweALT  7884  curry1  8013  curry2  8016  tposfn2  8135  frrlem11  8183  frrlem12  8184  fpr1  8190  wfrlem13OLD  8223  wfr1OLD  8229  tfrlem10  8289  tfr1  8299  frfnom  8337  undifixp  8794  sbthlem9  8957  fodomr  8994  frr1  9617  rankf  9652  cardf2  9801  axdc3lem2  10309  nqerf  10788  axaddf  11003  axmulf  11004  uzrdgfni  13780  hashkf  14148  shftfn  14884  imasaddfnlem  17337  imasvscafn  17346  fntopon  22180  cnextf  23324  ftc1cn  25314  nofnbday  26907  scutf  27058  grporn  29172  ffsrn  31351  measdivcstALTV  32491  bnj1422  33116  satff  33671  fnsingle  34360  fnimage  34370  imageval  34371  dfrecs2  34391  dfrdg4  34392  bj-isrvec  35621  ftc1cnnc  36005  fnresfnco  44953  funcoressn  44954  afvco2  45086