Definition df-fn 6557

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6730, dffn3 6740, dffn4 6821, and dffn5 6961. (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 6549	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6548	. . 3 wff Fun 𝐴
5	1	cdm 5682	. . . 4 class dom 𝐴
6	5, 2	wceq 1534	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 394	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 205	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6589  fnsng  6611  fnprg  6618  fntpg  6619  fntp  6620  fncnv  6632  fneq1  6651  fneq2  6652  nffn  6659  fnfun  6660  fndm  6663  fnun  6674  fncoOLD  6679  fnssresb  6683  fnres  6688  idfn  6689  fn0  6692  mptfnf  6696  fnopabg  6698  sbcfng  6725  fdmrn  6760  fcoi1  6776  f00  6784  f1cnvcnv  6807  fores  6825  dff1o4  6851  foimacnv  6860  funfv  6989  fvimacnvALT  7070  respreima  7079  dff3  7114  fpr  7168  fnsnb  7180  fnprb  7225  fnex  7234  fliftf  7327  fnoprabg  7548  fiun  7956  f1iun  7957  f1oweALT  7986  curry1  8118  curry2  8121  tposfn2  8263  frrlem11  8311  frrlem12  8312  fpr1  8318  wfrlem13OLD  8351  wfr1OLD  8357  tfrlem10  8417  tfr1  8427  frfnom  8465  undifixp  8963  sbthlem9  9129  fodomr  9166  fodomfir  9370  frr1  9802  rankf  9837  cardf2  9986  axdc3lem2  10494  nqerf  10973  axaddf  11188  axmulf  11189  uzrdgfni  13978  hashkf  14349  shftfn  15078  imasaddfnlem  17543  imasvscafn  17552  fntopon  22917  cnextf  24061  ftc1cn  26069  nofnbday  27682  scutf  27842  noseqrdgfn  28280  grporn  30454  ffsrn  32643  measdivcstALTV  34058  bnj1422  34682  satff  35238  fnsingle  35743  fnimage  35753  imageval  35754  dfrecs2  35774  dfrdg4  35775  bj-isrvec  37001  ftc1cnnc  37393  fnresfnco  46656  funcoressn  46657  afvco2  46789