Definition df-fn 5378

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 5370	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5369	. . 3 wff Fun 𝐴
5	1	cdm 4772	. . . 4 class dom 𝐴
6	5, 2	wceq 1402	. . 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  5405  fnsng  5426  fnprg  5434  fntpg  5435  fntp  5436  fncnv  5445  fneq1  5467  fneq2  5468  nffn  5475  fnfun  5476  fndm  5478  fnun  5487  fnco  5489  fnssresb  5493  fnres  5498  fnresi  5499  fn0  5501  fnopabg  5505  sbcfng  5529  fcoi1  5570  f00  5582  f1cnvcnv  5607  fores  5623  dff1o4  5645  foimacnv  5655  fun11iun  5658  funfvdm  5763  respreima  5830  fpr  5891  fnex  5931  fliftf  5998  fdmrn  6027  fnoprabg  6182  tposfn2  6530  tfrlemibfn  6592  tfri1d  6599  tfr1onlembfn  6608  tfri1dALT  6615  tfrcllembfn  6621  sbthlemi9  7275  caseinl  7424  caseinr  7425  ctssdccl  7444  exmidfodomrlemim  7546  axaddf  8228  axmulf  8229  frecuzrdgtcl  10830  frecuzrdgtclt  10839  shftfn  11570  imasaddfnlemg  13615  fntopon  15051