Definition df-fn 6493

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6662, dffn3 6672, dffn4 6750, and dffn5 6890. (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 6485	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6484	. . 3 wff Fun 𝐴
5	1	cdm 5622	. . . 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  6520  fnsng  6542  fnprg  6549  fntpg  6550  fntp  6551  fncnv  6563  fneq1  6581  fneq2  6582  nffn  6589  fnfun  6590  fndm  6593  fnun  6604  fnssresb  6612  fnres  6617  idfn  6618  fn0  6621  mptfnf  6625  fnopabg  6627  sbcfng  6657  fdmrn  6691  fcoi1  6706  f00  6714  f1cnvcnv  6737  fores  6754  dff1o4  6780  foimacnv  6789  funfv  6919  fvimacnvALT  7000  respreima  7009  dff3  7043  fpr  7097  fnsnbOLD  7110  fnprb  7152  fnex  7161  fliftf  7259  fnoprabg  7479  fiun  7885  f1iun  7886  f1oweALT  7914  curry1  8044  curry2  8047  tposfn2  8188  frrlem11  8236  frrlem12  8237  fpr1  8243  tfrlem10  8316  tfr1  8326  frfnom  8364  undifixp  8870  sbthlem9  9021  fodomr  9054  fodomfir  9226  frr1  9669  rankf  9704  cardf2  9853  axdc3lem2  10359  nqerf  10839  axaddf  11054  axmulf  11055  uzrdgfni  13879  hashkf  14253  shftfn  14994  imasaddfnlem  17447  imasvscafn  17456  nfchnd  18532  fntopon  22866  cnextf  24008  ftc1cn  26004  nofnbday  27618  scutf  27780  onsiso  28236  noseqrdgfn  28267  bdayn0sf1o  28328  grporn  30545  ffsrn  32756  measdivcstALTV  34331  bnj1422  34942  satff  35553  fnsingle  36060  fnimage  36070  imageval  36071  dfrecs2  36093  dfrdg4  36094  bj-isrvec  37438  ftc1cnnc  37832  modelaxreplem1  45161  fnresfnco  47229  funcoressn  47230  afvco2  47364