Definition df-fn 6558

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

This definition is used by:  funfn  6587  fnsng  6611  fnprg  6618  fntpg  6619  fntp  6620  fncnv  6632  fneq1  6649  fneq2  6650  nffn  6657  fnfun  6658  fndm  6661  fnun  6672  fnssresb  6680  fnres  6685  idfn  6686  fn0  6689  mptfnf  6693  fnopabg  6695  sbcfng  6725  fdmrn  6760  fcoi1  6775  f00  6783  f1cnvcnv  6808  fores  6825  dff1o4  6852  foimacnv  6861  funfv  6992  fvimacnvALT  7076  respreima  7086  dff3  7121  fpr  7179  fnprb  7234  fnex  7243  fliftf  7343  fnoprabg  7563  fiun  7976  f1iun  7977  f1oweALT  8005  curry1  8139  curry2  8142  tposfn2  8290  frrlem11  8339  frrlem12  8340  fpr1  8346  tfrlem10  8420  tfr1  8430  frfnom  8468  undifixp  8987  sbthlem9  9139  fodomr  9172  fodomfir  9344  frr1  9787  rankf  9826  cardf2  10048  axdc3lem2  10553  nqerf  11039  axaddf  11254  axmulf  11255  uzrdgfni  14125  hashkf  14500  shftfn  15252  sgnfo  15278  imasaddfnlem  17726  imasvscafn  17735  nfchnd  18811  mgmn0plusgf  18853  degenmgmnfn  19162  fntopon  23269  cnextf  24412  ftc1cn  26390  nofnbday  28036  cutsf  28205  oniso  28684  noseqrdgfn  28719  bdayn0sf1o  28783  grporn  31150  ffsrn  33387  measdivcstALTV  34925  bnj1422  35534  rncardr1prc  35849  acwer1prc  35851  satff  36341  fnsingle  36858  fnimage  36868  imageval  36869  dfrecs2  36891  dfrdg4  36892  bj-isrvec  38406  ftc1cnnc  38801  modelaxreplem1  46161  fnresfnco  48314  funcoressn  48315  afvco2  48449