Definition df-fn 5262

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 5254	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5253	. . 3 wff Fun 𝐴
5	1	cdm 4664	. . . 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  5289  fnsng  5306  fnprg  5314  fntpg  5315  fntp  5316  fncnv  5325  fneq1  5347  fneq2  5348  nffn  5355  fnfun  5356  fndm  5358  fnun  5367  fnco  5369  fnssresb  5373  fnres  5377  fnresi  5378  fn0  5380  fnopabg  5384  sbcfng  5408  fcoi1  5441  f00  5452  f1cnvcnv  5477  fores  5493  dff1o4  5515  foimacnv  5525  fun11iun  5528  funfvdm  5627  respreima  5693  fpr  5747  fnex  5787  fliftf  5849  fnoprabg  6027  tposfn2  6333  tfrlemibfn  6395  tfri1d  6402  tfr1onlembfn  6411  tfri1dALT  6418  tfrcllembfn  6424  sbthlemi9  7040  caseinl  7166  caseinr  7167  ctssdccl  7186  exmidfodomrlemim  7280  axaddf  7952  axmulf  7953  frecuzrdgtcl  10521  frecuzrdgtclt  10530  shftfn  11006  imasaddfnlemg  13016  fntopon  14344