Definition df-fn 6485

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6654, dffn3 6664, dffn4 6742, and dffn5 6881. (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 6477	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6476	. . 3 wff Fun 𝐴
5	1	cdm 5619	. . . 4 class dom 𝐴
6	5, 2	wceq 1540	. . 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  6512  fnsng  6534  fnprg  6541  fntpg  6542  fntp  6543  fncnv  6555  fneq1  6573  fneq2  6574  nffn  6581  fnfun  6582  fndm  6585  fnun  6596  fnssresb  6604  fnres  6609  idfn  6610  fn0  6613  mptfnf  6617  fnopabg  6619  sbcfng  6649  fdmrn  6683  fcoi1  6698  f00  6706  f1cnvcnv  6729  fores  6746  dff1o4  6772  foimacnv  6781  funfv  6910  fvimacnvALT  6991  respreima  7000  dff3  7034  fpr  7088  fnsnbOLD  7102  fnprb  7144  fnex  7153  fliftf  7252  fnoprabg  7472  fiun  7878  f1iun  7879  f1oweALT  7907  curry1  8037  curry2  8040  tposfn2  8181  frrlem11  8229  frrlem12  8230  fpr1  8236  tfrlem10  8309  tfr1  8319  frfnom  8357  undifixp  8861  sbthlem9  9012  fodomr  9045  fodomfir  9218  frr1  9655  rankf  9690  cardf2  9839  axdc3lem2  10345  nqerf  10824  axaddf  11039  axmulf  11040  uzrdgfni  13865  hashkf  14239  shftfn  14980  imasaddfnlem  17432  imasvscafn  17441  fntopon  22809  cnextf  23951  ftc1cn  25948  nofnbday  27562  scutf  27723  onsiso  28174  noseqrdgfn  28205  bdayn0sf1o  28264  grporn  30465  ffsrn  32673  measdivcstALTV  34198  bnj1422  34810  satff  35393  fnsingle  35903  fnimage  35913  imageval  35914  dfrecs2  35934  dfrdg4  35935  bj-isrvec  37278  ftc1cnnc  37682  modelaxreplem1  44962  fnresfnco  47035  funcoressn  47036  afvco2  47170