Definition df-fn 5282

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 5274	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5273	. . 3 wff Fun 𝐴
5	1	cdm 4682	. . . 4 class dom 𝐴
6	5, 2	wceq 1373	. . 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  5309  fnsng  5329  fnprg  5337  fntpg  5338  fntp  5339  fncnv  5348  fneq1  5370  fneq2  5371  nffn  5378  fnfun  5379  fndm  5381  fnun  5390  fnco  5392  fnssresb  5396  fnres  5401  fnresi  5402  fn0  5404  fnopabg  5408  sbcfng  5432  fcoi1  5467  f00  5478  f1cnvcnv  5503  fores  5519  dff1o4  5541  foimacnv  5551  fun11iun  5554  funfvdm  5654  respreima  5720  fpr  5778  fnex  5818  fliftf  5880  fnoprabg  6058  tposfn2  6364  tfrlemibfn  6426  tfri1d  6433  tfr1onlembfn  6442  tfri1dALT  6449  tfrcllembfn  6455  sbthlemi9  7081  caseinl  7207  caseinr  7208  ctssdccl  7227  exmidfodomrlemim  7324  axaddf  7996  axmulf  7997  frecuzrdgtcl  10574  frecuzrdgtclt  10583  shftfn  11205  imasaddfnlemg  13216  fntopon  14566