Definition df-fn 5084

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 5076	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5075	. . 3 wff Fun 𝐴
5	1	cdm 4499	. . . 4 class dom 𝐴
6	5, 2	wceq 1314	. . 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  5111  fnsng  5128  fnprg  5136  fntpg  5137  fntp  5138  fncnv  5147  fneq1  5169  fneq2  5170  nffn  5177  fnfun  5178  fndm  5180  fnun  5187  fnco  5189  fnssresb  5193  fnres  5197  fnresi  5198  fn0  5200  fnopabg  5204  sbcfng  5228  fcoi1  5261  f00  5272  f1cnvcnv  5297  fores  5312  dff1o4  5331  foimacnv  5341  fun11iun  5344  funfvdm  5438  respreima  5502  fpr  5556  fnex  5596  fliftf  5654  fnoprabg  5826  tposfn2  6117  tfrlemibfn  6179  tfri1d  6186  tfr1onlembfn  6195  tfri1dALT  6202  tfrcllembfn  6208  sbthlemi9  6805  caseinl  6928  caseinr  6929  ctssdccl  6948  exmidfodomrlemim  7005  axaddf  7603  axmulf  7604  frecuzrdgtcl  10078  frecuzrdgtclt  10087  shftfn  10489  fntopon  12034