Definition df-fn 5191

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 5183	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5182	. . 3 wff Fun 𝐴
5	1	cdm 4604	. . . 4 class dom 𝐴
6	5, 2	wceq 1343	. . 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  5218  fnsng  5235  fnprg  5243  fntpg  5244  fntp  5245  fncnv  5254  fneq1  5276  fneq2  5277  nffn  5284  fnfun  5285  fndm  5287  fnun  5294  fnco  5296  fnssresb  5300  fnres  5304  fnresi  5305  fn0  5307  fnopabg  5311  sbcfng  5335  fcoi1  5368  f00  5379  f1cnvcnv  5404  fores  5419  dff1o4  5440  foimacnv  5450  fun11iun  5453  funfvdm  5549  respreima  5613  fpr  5667  fnex  5707  fliftf  5767  fnoprabg  5943  tposfn2  6234  tfrlemibfn  6296  tfri1d  6303  tfr1onlembfn  6312  tfri1dALT  6319  tfrcllembfn  6325  sbthlemi9  6930  caseinl  7056  caseinr  7057  ctssdccl  7076  exmidfodomrlemim  7157  axaddf  7809  axmulf  7810  frecuzrdgtcl  10347  frecuzrdgtclt  10356  shftfn  10766  fntopon  12662