Definition df-fn 4986

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 4978	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 4977	. . 3 wff Fun 𝐴
5	1	cdm 4413	. . . 4 class dom 𝐴
6	5, 2	wceq 1287	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 102	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 103	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5012  fnsng  5028  fnprg  5036  fntpg  5037  fntp  5038  fncnv  5047  fneq1  5069  fneq2  5070  nffn  5077  fnfun  5078  fndm  5080  fnun  5087  fnco  5089  fnssresb  5093  fnres  5097  fnresi  5098  fn0  5100  fnopabg  5104  sbcfng  5126  fcoi1  5156  f00  5167  f1cnvcnv  5192  fores  5207  dff1o4  5226  foimacnv  5236  fun11iun  5239  funfvdm  5332  respreima  5392  fpr  5444  fnex  5482  fliftf  5541  fnoprabg  5705  tposfn2  5987  tfrlemibfn  6049  tfri1d  6056  tfr1onlembfn  6065  tfri1dALT  6072  tfrcllembfn  6078  sbthlemi9  6621  exmidfodomrlemim  6774  frecuzrdgtcl  9750  frecuzrdgtclt  9759  shftfn  10158