Definition df-fn 6499

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6668, dffn3 6678, dffn4 6756, and dffn5 6896. (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 6491	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6490	. . 3 wff Fun 𝐴
5	1	cdm 5628	. . . 4 class dom 𝐴
6	5, 2	wceq 1542	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 395	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 206	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6526  fnsng  6548  fnprg  6555  fntpg  6556  fntp  6557  fncnv  6569  fneq1  6587  fneq2  6588  nffn  6595  fnfun  6596  fndm  6599  fnun  6610  fnssresb  6618  fnres  6623  idfn  6624  fn0  6627  mptfnf  6631  fnopabg  6633  sbcfng  6663  fdmrn  6697  fcoi1  6712  f00  6720  f1cnvcnv  6743  fores  6760  dff1o4  6786  foimacnv  6795  funfv  6925  fvimacnvALT  7007  respreima  7016  dff3  7050  fpr  7105  fnsnbOLD  7118  fnprb  7160  fnex  7169  fliftf  7267  fnoprabg  7487  fiun  7893  f1iun  7894  f1oweALT  7922  curry1  8051  curry2  8054  tposfn2  8195  frrlem11  8243  frrlem12  8244  fpr1  8250  tfrlem10  8323  tfr1  8333  frfnom  8371  undifixp  8879  sbthlem9  9030  fodomr  9063  fodomfir  9235  frr1  9680  rankf  9715  cardf2  9864  axdc3lem2  10370  nqerf  10850  axaddf  11065  axmulf  11066  uzrdgfni  13917  hashkf  14291  shftfn  15032  imasaddfnlem  17489  imasvscafn  17498  nfchnd  18574  fntopon  22886  cnextf  24028  ftc1cn  26007  nofnbday  27613  cutsf  27781  oniso  28260  noseqrdgfn  28295  bdayn0sf1o  28359  grporn  30589  ffsrn  32798  measdivcstALTV  34366  bnj1422  34976  satff  35589  fnsingle  36096  fnimage  36106  imageval  36107  dfrecs2  36129  dfrdg4  36130  bj-isrvec  37605  ftc1cnnc  38010  modelaxreplem1  45402  fnresfnco  47480  funcoressn  47481  afvco2  47615