Definition df-fn 5850

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6004, dffn3 6011, dffn4 6078, and dffn5 6198. (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 5842	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5841	. . 3 wff Fun 𝐴
5	1	cdm 5074	. . . 4 class dom 𝐴
6	5, 2	wceq 1480	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 384	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 196	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5877  fnsng  5896  fnprg  5905  fntpg  5906  fntp  5907  fncnv  5920  fneq1  5937  fneq2  5938  nffn  5945  fnfun  5946  fndm  5948  fnun  5955  fnco  5957  fnssresb  5961  fnres  5965  fnresi  5966  fn0  5968  mptfnf  5972  fnopabg  5974  sbcfng  5999  fdmrn  6021  fcoi1  6035  f00  6044  f1cnvcnv  6066  fores  6081  dff1o4  6102  foimacnv  6111  funfv  6222  fvimacnvALT  6292  respreima  6300  dff3  6328  fpr  6375  fnsnb  6386  fnprb  6426  fnex  6435  fliftf  6519  fnoprabg  6714  fun11iun  7073  f1oweALT  7097  curry1  7214  curry2  7217  tposfn2  7319  wfrlem13  7372  wfr1  7378  tfrlem10  7428  tfr1  7438  frfnom  7475  undifixp  7888  sbthlem9  8022  fodomr  8055  rankf  8601  cardf2  8713  axdc3lem2  9217  nqerf  9696  axaddf  9910  axmulf  9911  uzrdgfni  12697  hashkf  13059  shftfn  13747  imasaddfnlem  16109  imasvscafn  16118  cnextf  21780  ftc1cn  23710  grporn  27221  ffsrn  29344  measdivcstOLD  30065  bnj145OLD  30500  bnj1422  30613  nofnbday  31503  elno2  31505  bdayfn  31539  fnsingle  31665  fnimage  31675  imageval  31676  dfrecs2  31696  dfrdg4  31697  bj-fntopon  32696  ftc1cnnc  33113  fnresfnco  40507  funcoressn  40508  afvco2  40557