Definition df-fn 5327

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 5319	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5318	. . 3 wff Fun 𝐴
5	1	cdm 4723	. . . 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  5354  fnsng  5374  fnprg  5382  fntpg  5383  fntp  5384  fncnv  5393  fneq1  5415  fneq2  5416  nffn  5423  fnfun  5424  fndm  5426  fnun  5435  fnco  5437  fnssresb  5441  fnres  5446  fnresi  5447  fn0  5449  fnopabg  5453  sbcfng  5477  fcoi1  5514  f00  5525  f1cnvcnv  5550  fores  5566  dff1o4  5588  foimacnv  5598  fun11iun  5601  funfvdm  5705  respreima  5771  fpr  5831  fnex  5871  fliftf  5935  fnoprabg  6117  tposfn2  6427  tfrlemibfn  6489  tfri1d  6496  tfr1onlembfn  6505  tfri1dALT  6512  tfrcllembfn  6518  sbthlemi9  7155  caseinl  7281  caseinr  7282  ctssdccl  7301  exmidfodomrlemim  7402  axaddf  8078  axmulf  8079  frecuzrdgtcl  10664  frecuzrdgtclt  10673  shftfn  11375  imasaddfnlemg  13387  fntopon  14738