Definition df-fn 2433

Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27.

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 2417	. 2 wff A Fn B
4	1	wfun 2416	. . 3 wff Fun A
5	1	cdm 2410	. . . 4 class dom A
6	5, 2	wceq 1091	. . 3 wff dom A = B
7	4, 6	wa 196	. 2 wff (Fun A ∧ dom A = B)
8	3, 7	wb 127	1 wff (A Fn B ↔ (Fun A ∧ dom A = B))

This definition is referenced by:  funfn 2689  fneq1 2718  fneq2 2719  hbfn 2720  fnfun 2721  fndm 2723  fnun 2730  fnssres 2734  fnresi 2737  fn0 2739  funex 2741  fnopabg 2745  fco 2760  f00 2773  fconst 2774  f1cnv 2782  funforn 2792  fores 2794  f1o4 2807  f1ocnv 2811  f1oco 2816  f1osn 2827  funfvop 2857  funfv 2862  fvi 2900  f1oweOLD 2944  tfrlem10 2958  tfr1 2962  frfnom 2989  fnoprab 3038  sbthlem9 3357  fodomb 3615  infxpidmlem7 4939

metamath.org