Definition df-fn 6543

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 6716, dffn3 6727, dffn4 6808, and dffn5 6947. (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 6535	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 6534	. . 3 wff Fun 𝐴
5	1	cdm 5675	. . . 4 class dom 𝐴
6	5, 2	wceq 1542	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 397	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 205	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  6575  fnsng  6597  fnprg  6604  fntpg  6605  fntp  6606  fncnv  6618  fneq1  6637  fneq2  6638  nffn  6645  fnfun  6646  fndm  6649  fnun  6660  fncoOLD  6665  fnssresb  6669  fnres  6674  idfn  6675  fn0  6678  mptfnf  6682  fnopabg  6684  sbcfng  6711  fdmrn  6746  fcoi1  6762  f00  6770  f1cnvcnv  6794  fores  6812  dff1o4  6838  foimacnv  6847  funfv  6974  fvimacnvALT  7054  respreima  7063  dff3  7097  fpr  7147  fnsnb  7159  fnprb  7205  fnex  7214  fliftf  7307  fnoprabg  7526  fiun  7924  f1iun  7925  f1oweALT  7954  curry1  8085  curry2  8088  tposfn2  8228  frrlem11  8276  frrlem12  8277  fpr1  8283  wfrlem13OLD  8316  wfr1OLD  8322  tfrlem10  8382  tfr1  8392  frfnom  8430  undifixp  8924  sbthlem9  9087  fodomr  9124  frr1  9750  rankf  9785  cardf2  9934  axdc3lem2  10442  nqerf  10921  axaddf  11136  axmulf  11137  uzrdgfni  13919  hashkf  14288  shftfn  15016  imasaddfnlem  17470  imasvscafn  17479  fntopon  22408  cnextf  23552  ftc1cn  25542  nofnbday  27135  scutf  27293  grporn  29752  ffsrn  31932  measdivcstALTV  33161  bnj1422  33786  satff  34339  fnsingle  34829  fnimage  34839  imageval  34840  dfrecs2  34860  dfrdg4  34861  bj-isrvec  36113  ftc1cnnc  36498  fnresfnco  45686  funcoressn  45687  afvco2  45819