Definition df-fn 4905

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 4897	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 4896	. . 3 wff Fun 𝐴
5	1	cdm 4345	. . . 4 class dom 𝐴
6	5, 2	wceq 1243	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 97	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 98	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  4931  fnsng  4947  fnprg  4954  fntpg  4955  fntp  4956  fncnv  4965  fneq1  4987  fneq2  4988  nffn  4995  fnfun  4996  fndm  4998  fnun  5005  fnco  5007  fnssresb  5011  fnres  5015  fnresi  5016  fn0  5018  fnopabg  5022  sbcfng  5044  fcoi1  5070  f00  5081  f1cnvcnv  5100  fores  5115  dff1o4  5134  foimacnv  5144  fun11iun  5147  funfvdm  5236  respreima  5295  fpr  5345  fnex  5383  fliftf  5439  fnoprabg  5602  tposfn2  5881  tfrlemibfn  5942  tfri1d  5949  frecuzrdgfn  9198  shftfn  9425