Definition df-fn 6489

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6658, dffn3 6668, 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 6481	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6480	. . 3 wff Fun 𝐴
5	1	cdm 5623	. . . 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  6516  fnsng  6538  fnprg  6545  fntpg  6546  fntp  6547  fncnv  6559  fneq1  6577  fneq2  6578  nffn  6585  fnfun  6586  fndm  6589  fnun  6600  fnssresb  6608  fnres  6613  idfn  6614  fn0  6617  mptfnf  6621  fnopabg  6623  sbcfng  6653  fdmrn  6687  fcoi1  6702  f00  6710  f1cnvcnv  6733  fores  6750  dff1o4  6776  foimacnv  6785  funfv  6914  fvimacnvALT  6995  respreima  7004  dff3  7038  fpr  7092  fnsnbOLD  7106  fnprb  7148  fnex  7157  fliftf  7256  fnoprabg  7476  fiun  7885  f1iun  7886  f1oweALT  7914  curry1  8044  curry2  8047  tposfn2  8188  frrlem11  8236  frrlem12  8237  fpr1  8243  tfrlem10  8316  tfr1  8326  frfnom  8364  undifixp  8868  sbthlem9  9019  fodomr  9052  fodomfir  9237  frr1  9674  rankf  9709  cardf2  9858  axdc3lem2  10364  nqerf  10843  axaddf  11058  axmulf  11059  uzrdgfni  13884  hashkf  14258  shftfn  14999  imasaddfnlem  17451  imasvscafn  17460  fntopon  22828  cnextf  23970  ftc1cn  25967  nofnbday  27581  scutf  27742  onsiso  28193  noseqrdgfn  28224  bdayn0sf1o  28283  grporn  30484  ffsrn  32691  measdivcstALTV  34211  bnj1422  34823  satff  35402  fnsingle  35912  fnimage  35922  imageval  35923  dfrecs2  35943  dfrdg4  35944  bj-isrvec  37287  ftc1cnnc  37691  modelaxreplem1  44972  fnresfnco  47045  funcoressn  47046  afvco2  47180