Definition df-fn 6541

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6711, dffn3 6722, dffn4 6802, and dffn5 6943. (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 6533	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6532	. . 3 wff Fun 𝐴
5	1	cdm 5650	. . . 4 class dom 𝐴
6	5, 2	wceq 1569	. . 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  6570  fnsng  6592  fnprg  6599  fntpg  6600  fntp  6601  fncnv  6613  fneq1  6630  fneq2  6631  nffn  6638  fnfun  6639  fndm  6642  fnun  6653  fnssresb  6661  fnres  6666  idfn  6667  fn0  6670  mptfnf  6674  fnopabg  6676  sbcfng  6706  fdmrn  6741  fcoi1  6756  f00  6764  f1cnvcnv  6789  fores  6806  dff1o4  6833  foimacnv  6842  funfv  6972  fvimacnvALT  7056  respreima  7065  dff3  7100  fpr  7158  fnsnbOLD  7171  fnprb  7214  fnex  7223  fliftf  7323  fnoprabg  7543  fiun  7955  f1iun  7956  f1oweALT  7984  curry1  8115  curry2  8118  tposfn2  8265  frrlem11  8314  frrlem12  8315  fpr1  8321  tfrlem10  8395  tfr1  8405  frfnom  8443  undifixp  8962  sbthlem9  9114  fodomr  9147  fodomfir  9319  frr1  9763  rankf  9802  cardf2  10024  axdc3lem2  10529  nqerf  11015  axaddf  11230  axmulf  11231  uzrdgfni  14101  hashkf  14476  shftfn  15226  sgnfo  15252  imasaddfnlem  17700  imasvscafn  17709  nfchnd  18785  mgmn0plusgf  18827  degenmgmnfn  19136  fntopon  23242  cnextf  24385  ftc1cn  26363  nofnbday  28009  cutsf  28178  oniso  28657  noseqrdgfn  28692  bdayn0sf1o  28756  grporn  31123  ffsrn  33362  measdivcstALTV  34900  bnj1422  35509  rncardr1prc  35800  acwer1prc  35802  satff  36217  fnsingle  36723  fnimage  36733  imageval  36734  dfrecs2  36756  dfrdg4  36757  bj-isrvec  38258  ftc1cnnc  38653  modelaxreplem1  46010  fnresfnco  48153  funcoressn  48154  afvco2  48288