Definition df-fn 5238

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 5230	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5229	. . 3 wff Fun 𝐴
5	1	cdm 4644	. . . 4 class dom 𝐴
6	5, 2	wceq 1364	. . 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  5265  fnsng  5282  fnprg  5290  fntpg  5291  fntp  5292  fncnv  5301  fneq1  5323  fneq2  5324  nffn  5331  fnfun  5332  fndm  5334  fnun  5341  fnco  5343  fnssresb  5347  fnres  5351  fnresi  5352  fn0  5354  fnopabg  5358  sbcfng  5382  fcoi1  5415  f00  5426  f1cnvcnv  5451  fores  5466  dff1o4  5488  foimacnv  5498  fun11iun  5501  funfvdm  5600  respreima  5665  fpr  5719  fnex  5759  fliftf  5821  fnoprabg  5997  tposfn2  6291  tfrlemibfn  6353  tfri1d  6360  tfr1onlembfn  6369  tfri1dALT  6376  tfrcllembfn  6382  sbthlemi9  6994  caseinl  7120  caseinr  7121  ctssdccl  7140  exmidfodomrlemim  7230  axaddf  7897  axmulf  7898  frecuzrdgtcl  10443  frecuzrdgtclt  10452  shftfn  10865  imasaddfnlemg  12791  fntopon  13981