Definition df-fn 5336

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 5328	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5327	. . 3 wff Fun 𝐴
5	1	cdm 4731	. . . 4 class dom 𝐴
6	5, 2	wceq 1398	. . 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  5363  fnsng  5384  fnprg  5392  fntpg  5393  fntp  5394  fncnv  5403  fneq1  5425  fneq2  5426  nffn  5433  fnfun  5434  fndm  5436  fnun  5445  fnco  5447  fnssresb  5451  fnres  5456  fnresi  5457  fn0  5459  fnopabg  5463  sbcfng  5487  fcoi1  5525  f00  5537  f1cnvcnv  5562  fores  5578  dff1o4  5600  foimacnv  5610  fun11iun  5613  funfvdm  5718  respreima  5783  fpr  5844  fnex  5884  fliftf  5950  fnoprabg  6132  tposfn2  6475  tfrlemibfn  6537  tfri1d  6544  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  sbthlemi9  7207  caseinl  7350  caseinr  7351  ctssdccl  7370  exmidfodomrlemim  7472  axaddf  8148  axmulf  8149  frecuzrdgtcl  10737  frecuzrdgtclt  10746  shftfn  11464  imasaddfnlemg  13477  fntopon  14835