Definition df-fn 4828

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	⊢ (A Fn B ↔ (Fun A ∧ dom A = B))

Detailed syntax breakdown of Definition df-fn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wfn 4820	. 2 wff A Fn B
4	1	wfun 4819	. . 3 wff Fun A
5	1	cdm 4268	. . . 4 class dom A
6	5, 2	wceq 1226	. . 3 wff dom A = B
7	4, 6	wa 97	. 2 wff (Fun A ∧ dom A = B)
8	3, 7	wb 98	1 wff (A Fn B ↔ (Fun A ∧ dom A = B))

This definition is referenced by:  funfn  4853  fnsng  4869  fnprg  4876  fntpg  4877  fntp  4878  fncnv  4887  fneq1  4909  fneq2  4910  nffn  4917  fnfun  4918  fndm  4920  fnun  4927  fnco  4929  fnssresb  4933  fnres  4937  fnresi  4938  fn0  4940  fnopabg  4944  sbcfng  4966  fcoi1  4991  f00  5002  f1cnvcnv  5021  fores  5036  dff1o4  5055  foimacnv  5065  fun11iun  5068  funfvdm  5157  respreima  5216  fpr  5266  fnex  5304  fliftf  5360  fnoprabg  5521  tposfn2  5799  tfrlemibfn  5859  tfri1d  5867  tfri1  5869