Definition df-fn 6565

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6738, dffn3 6748, dffn4 6826, and dffn5 6966. (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 6557	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6556	. . 3 wff Fun 𝐴
5	1	cdm 5688	. . . 4 class dom 𝐴
6	5, 2	wceq 1536	. . 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  6597  fnsng  6619  fnprg  6626  fntpg  6627  fntp  6628  fncnv  6640  fneq1  6659  fneq2  6660  nffn  6667  fnfun  6668  fndm  6671  fnun  6682  fnssresb  6690  fnres  6695  idfn  6696  fn0  6699  mptfnf  6703  fnopabg  6705  sbcfng  6733  fdmrn  6767  fcoi1  6782  f00  6790  f1cnvcnv  6813  fores  6830  dff1o4  6856  foimacnv  6865  funfv  6995  fvimacnvALT  7076  respreima  7085  dff3  7119  fpr  7173  fnsnb  7185  fnprb  7227  fnex  7236  fliftf  7334  fnoprabg  7555  fiun  7965  f1iun  7966  f1oweALT  7995  curry1  8127  curry2  8130  tposfn2  8271  frrlem11  8319  frrlem12  8320  fpr1  8326  wfrlem13OLD  8359  wfr1OLD  8365  tfrlem10  8425  tfr1  8435  frfnom  8473  undifixp  8972  sbthlem9  9129  fodomr  9166  fodomfir  9365  frr1  9796  rankf  9831  cardf2  9980  axdc3lem2  10488  nqerf  10967  axaddf  11182  axmulf  11183  uzrdgfni  13995  hashkf  14367  shftfn  15108  imasaddfnlem  17574  imasvscafn  17583  fntopon  22945  cnextf  24089  ftc1cn  26098  nofnbday  27711  scutf  27871  noseqrdgfn  28326  grporn  30549  ffsrn  32746  measdivcstALTV  34205  bnj1422  34829  satff  35394  fnsingle  35900  fnimage  35910  imageval  35911  dfrecs2  35931  dfrdg4  35932  bj-isrvec  37276  ftc1cnnc  37678  modelaxreplem1  44942  fnresfnco  46990  funcoressn  46991  afvco2  47125