Definition df-fn 5216

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 5208	. 2 wff 𝐴 Fn 𝐵
4	1	wfun 5207	. . 3 wff Fun 𝐴
5	1	cdm 4624	. . . 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  5243  fnsng  5260  fnprg  5268  fntpg  5269  fntp  5270  fncnv  5279  fneq1  5301  fneq2  5302  nffn  5309  fnfun  5310  fndm  5312  fnun  5319  fnco  5321  fnssresb  5325  fnres  5329  fnresi  5330  fn0  5332  fnopabg  5336  sbcfng  5360  fcoi1  5393  f00  5404  f1cnvcnv  5429  fores  5444  dff1o4  5466  foimacnv  5476  fun11iun  5479  funfvdm  5576  respreima  5641  fpr  5695  fnex  5735  fliftf  5795  fnoprabg  5971  tposfn2  6262  tfrlemibfn  6324  tfri1d  6331  tfr1onlembfn  6340  tfri1dALT  6347  tfrcllembfn  6353  sbthlemi9  6959  caseinl  7085  caseinr  7086  ctssdccl  7105  exmidfodomrlemim  7195  axaddf  7862  axmulf  7863  frecuzrdgtcl  10405  frecuzrdgtclt  10414  shftfn  10824  fntopon  13304