Definition df-fn 4820

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 4812	. 2 wff A Fn B
4	1	wfun 4811	. . 3 wff Fun A
5	1	cdm 4260	. . . 4 class dom A
6	5, 2	wceq 1223	. . 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  4845  fnsng  4861  fnprg  4868  fntpg  4869  fntp  4870  fncnv  4879  fneq1  4901  fneq2  4902  nffn  4909  fnfun  4910  fndm  4912  fnun  4919  fnco  4921  fnssresb  4925  fnres  4929  fnresi  4930  fn0  4932  fnopabg  4936  sbcfng  4958  fcoi1  4983  f00  4994  f1cnvcnv  5013  fores  5028  dff1o4  5047  foimacnv  5057  fun11iun  5060  funfvdm  5149  respreima  5208  fpr  5258  fnex  5296  fliftf  5352  fnoprabg  5513  tposfn2  5791  tfrlemibfn  5851  tfri1d  5859  tfri1  5861