Definition df-fn 4848

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 4840	. 2 wff A Fn B
4	1	wfun 4839	. . 3 wff Fun A
5	1	cdm 4288	. . . 4 class dom A
6	5, 2	wceq 1242	. . 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  4874  fnsng  4890  fnprg  4897  fntpg  4898  fntp  4899  fncnv  4908  fneq1  4930  fneq2  4931  nffn  4938  fnfun  4939  fndm  4941  fnun  4948  fnco  4950  fnssresb  4954  fnres  4958  fnresi  4959  fn0  4961  fnopabg  4965  sbcfng  4987  fcoi1  5013  f00  5024  f1cnvcnv  5043  fores  5058  dff1o4  5077  foimacnv  5087  fun11iun  5090  funfvdm  5179  respreima  5238  fpr  5288  fnex  5326  fliftf  5382  fnoprabg  5544  tposfn2  5822  tfrlemibfn  5883  tfri1d  5890  frecuzrdgfn  8839