Definition df-fn 5321

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (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 5313	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5312	. . 3 wff Fun 𝐴
5	1	cdm 4719	. . . 4 class dom 𝐴
6	5, 2	wceq 1395	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 104	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 105	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5348  fnsng  5368  fnprg  5376  fntpg  5377  fntp  5378  fncnv  5387  fneq1  5409  fneq2  5410  nffn  5417  fnfun  5418  fndm  5420  fnun  5429  fnco  5431  fnssresb  5435  fnres  5440  fnresi  5441  fn0  5443  fnopabg  5447  sbcfng  5471  fcoi1  5508  f00  5519  f1cnvcnv  5544  fores  5560  dff1o4  5582  foimacnv  5592  fun11iun  5595  funfvdm  5699  respreima  5765  fpr  5825  fnex  5865  fliftf  5929  fnoprabg  6111  tposfn2  6418  tfrlemibfn  6480  tfri1d  6487  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  sbthlemi9  7143  caseinl  7269  caseinr  7270  ctssdccl  7289  exmidfodomrlemim  7390  axaddf  8066  axmulf  8067  frecuzrdgtcl  10646  frecuzrdgtclt  10655  shftfn  11350  imasaddfnlemg  13362  fntopon  14713