Definition df-fn 6484

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6653, dffn3 6663, dffn4 6741, and dffn5 6880. (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 6476	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6475	. . 3 wff Fun 𝐴
5	1	cdm 5614	. . . 4 class dom 𝐴
6	5, 2	wceq 1541	. . 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  6511  fnsng  6533  fnprg  6540  fntpg  6541  fntp  6542  fncnv  6554  fneq1  6572  fneq2  6573  nffn  6580  fnfun  6581  fndm  6584  fnun  6595  fnssresb  6603  fnres  6608  idfn  6609  fn0  6612  mptfnf  6616  fnopabg  6618  sbcfng  6648  fdmrn  6682  fcoi1  6697  f00  6705  f1cnvcnv  6728  fores  6745  dff1o4  6771  foimacnv  6780  funfv  6909  fvimacnvALT  6990  respreima  6999  dff3  7033  fpr  7087  fnsnbOLD  7100  fnprb  7142  fnex  7151  fliftf  7249  fnoprabg  7469  fiun  7875  f1iun  7876  f1oweALT  7904  curry1  8034  curry2  8037  tposfn2  8178  frrlem11  8226  frrlem12  8227  fpr1  8233  tfrlem10  8306  tfr1  8316  frfnom  8354  undifixp  8858  sbthlem9  9008  fodomr  9041  fodomfir  9212  frr1  9652  rankf  9687  cardf2  9836  axdc3lem2  10342  nqerf  10821  axaddf  11036  axmulf  11037  uzrdgfni  13865  hashkf  14239  shftfn  14980  imasaddfnlem  17432  imasvscafn  17441  nfchnd  18517  fntopon  22839  cnextf  23981  ftc1cn  25977  nofnbday  27591  scutf  27753  onsiso  28205  noseqrdgfn  28236  bdayn0sf1o  28295  grporn  30501  ffsrn  32711  measdivcstALTV  34238  bnj1422  34849  satff  35454  fnsingle  35961  fnimage  35971  imageval  35972  dfrecs2  35994  dfrdg4  35995  bj-isrvec  37338  ftc1cnnc  37742  modelaxreplem1  45081  fnresfnco  47151  funcoressn  47152  afvco2  47286