Definition df-fn 5283

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 5275	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5274	. . 3 wff Fun 𝐴
5	1	cdm 4683	. . . 4 class dom 𝐴
6	5, 2	wceq 1373	. . 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  5310  fnsng  5330  fnprg  5338  fntpg  5339  fntp  5340  fncnv  5349  fneq1  5371  fneq2  5372  nffn  5379  fnfun  5380  fndm  5382  fnun  5391  fnco  5393  fnssresb  5397  fnres  5402  fnresi  5403  fn0  5405  fnopabg  5409  sbcfng  5433  fcoi1  5468  f00  5479  f1cnvcnv  5504  fores  5520  dff1o4  5542  foimacnv  5552  fun11iun  5555  funfvdm  5655  respreima  5721  fpr  5779  fnex  5819  fliftf  5881  fnoprabg  6059  tposfn2  6365  tfrlemibfn  6427  tfri1d  6434  tfr1onlembfn  6443  tfri1dALT  6450  tfrcllembfn  6456  sbthlemi9  7082  caseinl  7208  caseinr  7209  ctssdccl  7228  exmidfodomrlemim  7325  axaddf  8001  axmulf  8002  frecuzrdgtcl  10579  frecuzrdgtclt  10588  shftfn  11210  imasaddfnlemg  13221  fntopon  14571