Definition df-f 5337

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 5329	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5328	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4732	. . . 4 class ran 𝐹
7	6, 2	wss 3201	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 104	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 105	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5472  feq2  5473  feq3  5474  nff  5486  sbcfg  5488  ffn  5489  dffn2  5491  frn  5498  dffn3  5500  fss  5501  fco  5507  funssxp  5512  fun  5516  fnfco  5519  fssres  5520  fcoi2  5526  fintm  5530  fin  5531  f0  5536  fconst  5541  f1ssr  5558  fof  5568  dff1o2  5597  fun11iun  5613  ffoss  5625  dff2  5799  fmpt  5805  ffnfv  5813  ffvresb  5818  fcof  5841  fpr  5844  fprg  5845  idref  5907  dff1o6  5927  fliftf  5950  1stcof  6335  2ndcof  6336  smores  6501  smores2  6503  iordsmo  6506  tfrcllembfn  6566  sbthlemi9  7207  inresflem  7319  frec2uzf1od  10731  frecuzrdgtcl  10737  fclim  11934  ennnfonelemf1  13119  resmhm2b  13652  srgfcl  14067  cnrest2  15047  lmss  15057  psmetxrge0  15143  dvfgg  15499  plyreres  15575  ausgrusgrben  16109  ausgrumgrien  16111  subuhgr  16213  subupgr  16214  subumgr  16215  subusgr  16216  nninfall  16735