Definition df-fn 6502

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6672, dffn3 6682, dffn4 6760, and dffn5 6901. (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 6494	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6493	. . 3 wff Fun 𝐴
5	1	cdm 5631	. . . 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  6530  fnsng  6552  fnprg  6559  fntpg  6560  fntp  6561  fncnv  6573  fneq1  6591  fneq2  6592  nffn  6599  fnfun  6600  fndm  6603  fnun  6614  fnssresb  6622  fnres  6627  idfn  6628  fn0  6631  mptfnf  6635  fnopabg  6637  sbcfng  6667  fdmrn  6701  fcoi1  6716  f00  6724  f1cnvcnv  6747  fores  6764  dff1o4  6790  foimacnv  6799  funfv  6930  fvimacnvALT  7011  respreima  7020  dff3  7054  fpr  7108  fnsnbOLD  7122  fnprb  7164  fnex  7173  fliftf  7272  fnoprabg  7492  fiun  7901  f1iun  7902  f1oweALT  7930  curry1  8060  curry2  8063  tposfn2  8204  frrlem11  8252  frrlem12  8253  fpr1  8259  tfrlem10  8332  tfr1  8342  frfnom  8380  undifixp  8884  sbthlem9  9036  fodomr  9069  fodomfir  9255  frr1  9688  rankf  9723  cardf2  9872  axdc3lem2  10380  nqerf  10859  axaddf  11074  axmulf  11075  uzrdgfni  13899  hashkf  14273  shftfn  15015  imasaddfnlem  17467  imasvscafn  17476  fntopon  22787  cnextf  23929  ftc1cn  25926  nofnbday  27540  scutf  27700  onsiso  28145  noseqrdgfn  28176  bdayn0sf1o  28235  grporn  30423  ffsrn  32625  measdivcstALTV  34188  bnj1422  34800  satff  35370  fnsingle  35880  fnimage  35890  imageval  35891  dfrecs2  35911  dfrdg4  35912  bj-isrvec  37255  ftc1cnnc  37659  modelaxreplem1  44941  fnresfnco  47015  funcoressn  47016  afvco2  47150