Definition df-fn 5219

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 5211	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5210	. . 3 wff Fun 𝐴
5	1	cdm 4626	. . . 4 class dom 𝐴
6	5, 2	wceq 1353	. . 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  5246  fnsng  5263  fnprg  5271  fntpg  5272  fntp  5273  fncnv  5282  fneq1  5304  fneq2  5305  nffn  5312  fnfun  5313  fndm  5315  fnun  5322  fnco  5324  fnssresb  5328  fnres  5332  fnresi  5333  fn0  5335  fnopabg  5339  sbcfng  5363  fcoi1  5396  f00  5407  f1cnvcnv  5432  fores  5447  dff1o4  5469  foimacnv  5479  fun11iun  5482  funfvdm  5579  respreima  5644  fpr  5698  fnex  5738  fliftf  5799  fnoprabg  5975  tposfn2  6266  tfrlemibfn  6328  tfri1d  6335  tfr1onlembfn  6344  tfri1dALT  6351  tfrcllembfn  6357  sbthlemi9  6963  caseinl  7089  caseinr  7090  ctssdccl  7109  exmidfodomrlemim  7199  axaddf  7866  axmulf  7867  frecuzrdgtcl  10411  frecuzrdgtclt  10420  shftfn  10832  imasaddfnlemg  12734  fntopon  13494