Definition df-fn 5211

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 5203	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5202	. . 3 wff Fun 𝐴
5	1	cdm 4620	. . . 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  5238  fnsng  5255  fnprg  5263  fntpg  5264  fntp  5265  fncnv  5274  fneq1  5296  fneq2  5297  nffn  5304  fnfun  5305  fndm  5307  fnun  5314  fnco  5316  fnssresb  5320  fnres  5324  fnresi  5325  fn0  5327  fnopabg  5331  sbcfng  5355  fcoi1  5388  f00  5399  f1cnvcnv  5424  fores  5439  dff1o4  5461  foimacnv  5471  fun11iun  5474  funfvdm  5571  respreima  5636  fpr  5690  fnex  5730  fliftf  5790  fnoprabg  5966  tposfn2  6257  tfrlemibfn  6319  tfri1d  6326  tfr1onlembfn  6335  tfri1dALT  6342  tfrcllembfn  6348  sbthlemi9  6954  caseinl  7080  caseinr  7081  ctssdccl  7100  exmidfodomrlemim  7190  axaddf  7842  axmulf  7843  frecuzrdgtcl  10382  frecuzrdgtclt  10391  shftfn  10801  fntopon  13102