Definition df-fn 5329

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 5321	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5320	. . 3 wff Fun 𝐴
5	1	cdm 4725	. . . 4 class dom 𝐴
6	5, 2	wceq 1397	. . 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  5356  fnsng  5377  fnprg  5385  fntpg  5386  fntp  5387  fncnv  5396  fneq1  5418  fneq2  5419  nffn  5426  fnfun  5427  fndm  5429  fnun  5438  fnco  5440  fnssresb  5444  fnres  5449  fnresi  5450  fn0  5452  fnopabg  5456  sbcfng  5480  fcoi1  5517  f00  5528  f1cnvcnv  5553  fores  5569  dff1o4  5591  foimacnv  5601  fun11iun  5604  funfvdm  5709  respreima  5775  fpr  5835  fnex  5875  fliftf  5939  fnoprabg  6121  tposfn2  6431  tfrlemibfn  6493  tfri1d  6500  tfr1onlembfn  6509  tfri1dALT  6516  tfrcllembfn  6522  sbthlemi9  7163  caseinl  7289  caseinr  7290  ctssdccl  7309  exmidfodomrlemim  7411  axaddf  8087  axmulf  8088  frecuzrdgtcl  10673  frecuzrdgtclt  10682  shftfn  11384  imasaddfnlemg  13396  fntopon  14747