Definition df-fn 5320

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 5312	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5311	. . 3 wff Fun 𝐴
5	1	cdm 4718	. . . 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  5347  fnsng  5367  fnprg  5375  fntpg  5376  fntp  5377  fncnv  5386  fneq1  5408  fneq2  5409  nffn  5416  fnfun  5417  fndm  5419  fnun  5428  fnco  5430  fnssresb  5434  fnres  5439  fnresi  5440  fn0  5442  fnopabg  5446  sbcfng  5470  fcoi1  5505  f00  5516  f1cnvcnv  5541  fores  5557  dff1o4  5579  foimacnv  5589  fun11iun  5592  funfvdm  5696  respreima  5762  fpr  5820  fnex  5860  fliftf  5922  fnoprabg  6104  tposfn2  6410  tfrlemibfn  6472  tfri1d  6479  tfr1onlembfn  6488  tfri1dALT  6495  tfrcllembfn  6501  sbthlemi9  7128  caseinl  7254  caseinr  7255  ctssdccl  7274  exmidfodomrlemim  7375  axaddf  8051  axmulf  8052  frecuzrdgtcl  10629  frecuzrdgtclt  10638  shftfn  11330  imasaddfnlemg  13342  fntopon  14692