Definition df-fn 5221

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 5213	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5212	. . 3 wff Fun 𝐴
5	1	cdm 4628	. . . 4 class dom 𝐴
6	5, 2	wceq 1353	. . 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  5248  fnsng  5265  fnprg  5273  fntpg  5274  fntp  5275  fncnv  5284  fneq1  5306  fneq2  5307  nffn  5314  fnfun  5315  fndm  5317  fnun  5324  fnco  5326  fnssresb  5330  fnres  5334  fnresi  5335  fn0  5337  fnopabg  5341  sbcfng  5365  fcoi1  5398  f00  5409  f1cnvcnv  5434  fores  5449  dff1o4  5471  foimacnv  5481  fun11iun  5484  funfvdm  5581  respreima  5646  fpr  5700  fnex  5740  fliftf  5802  fnoprabg  5978  tposfn2  6269  tfrlemibfn  6331  tfri1d  6338  tfr1onlembfn  6347  tfri1dALT  6354  tfrcllembfn  6360  sbthlemi9  6966  caseinl  7092  caseinr  7093  ctssdccl  7112  exmidfodomrlemim  7202  axaddf  7869  axmulf  7870  frecuzrdgtcl  10414  frecuzrdgtclt  10423  shftfn  10835  imasaddfnlemg  12740  fntopon  13563