Definition df-fn 5201

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 5193	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5192	. . 3 wff Fun 𝐴
5	1	cdm 4611	. . . 4 class dom 𝐴
6	5, 2	wceq 1348	. . 3 wff dom 𝐴 = 𝐵
7	4, 6	wa 103	. 2 wff (Fun 𝐴 ∧ dom 𝐴 = 𝐵)
8	3, 7	wb 104	1 wff (𝐴 Fn 𝐵 ↔ (Fun 𝐴 ∧ dom 𝐴 = 𝐵))

This definition is referenced by:  funfn  5228  fnsng  5245  fnprg  5253  fntpg  5254  fntp  5255  fncnv  5264  fneq1  5286  fneq2  5287  nffn  5294  fnfun  5295  fndm  5297  fnun  5304  fnco  5306  fnssresb  5310  fnres  5314  fnresi  5315  fn0  5317  fnopabg  5321  sbcfng  5345  fcoi1  5378  f00  5389  f1cnvcnv  5414  fores  5429  dff1o4  5450  foimacnv  5460  fun11iun  5463  funfvdm  5559  respreima  5624  fpr  5678  fnex  5718  fliftf  5778  fnoprabg  5954  tposfn2  6245  tfrlemibfn  6307  tfri1d  6314  tfr1onlembfn  6323  tfri1dALT  6330  tfrcllembfn  6336  sbthlemi9  6942  caseinl  7068  caseinr  7069  ctssdccl  7088  exmidfodomrlemim  7178  axaddf  7830  axmulf  7831  frecuzrdgtcl  10368  frecuzrdgtclt  10377  shftfn  10788  fntopon  12816