Definition df-fn 3193

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 3177	. 2 wff A Fn B
4	1	wfun 3176	. . 3 wff Fun A
5	1	cdm 3170	. . . 4 class dom A
6	5, 2	wceq 956	. . 3 wff dom A = B
7	4, 6	wa 223	. 2 wff (Fun A /\ dom A = B)
8	3, 7	wb 146	1 wff (A Fn B <-> (Fun A /\ dom A = B))

This definition is referenced by:  funfn 3542  fncnv 3561  fneq1 3582  fneq2 3583  hbfn 3584  fnfun 3585  fndm 3587  fnun 3594  fnco 3595  fnssresb 3599  fnresi 3603  fn0 3605  fnopabg 3615  fco 3636  f00 3657  fconst 3658  f1cnv 3666  fores 3681  f1o4 3696  f1ocnv 3701  f1osn 3719  funbrfvb 3755  funfv 3770  fvimacnvALT 3809  dff2 3817  fvi 3842  f1oweALT 3906  tfrlem10 3920  tfr1 3924  frfnom 3951  fnoprabg 4012  curry1 4098  sbthlem9 4455  fodomr 4483  axaddopr 5265  axmulopr 5266  infxpidmlem7 7558  grprn 8056  ringsn 8163  cmpdom 10468  trnij 10637

Copyright terms: Public domain