Definition df-f 5284

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 5276	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5275	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4684	. . . 4 class ran 𝐹
7	6, 2	wss 3170	. . 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  5418  feq2  5419  feq3  5420  nff  5432  sbcfg  5434  ffn  5435  dffn2  5437  frn  5444  dffn3  5446  fss  5447  fco  5451  funssxp  5455  fun  5459  fnfco  5462  fssres  5463  fcoi2  5469  fintm  5473  fin  5474  f0  5478  fconst  5483  f1ssr  5500  fof  5510  dff1o2  5539  fun11iun  5555  ffoss  5566  dff2  5737  fmpt  5743  ffnfv  5751  ffvresb  5756  fpr  5779  fprg  5780  idref  5838  dff1o6  5858  fliftf  5881  1stcof  6262  2ndcof  6263  smores  6391  smores2  6393  iordsmo  6396  tfrcllembfn  6456  sbthlemi9  7082  inresflem  7177  frec2uzf1od  10573  frecuzrdgtcl  10579  fclim  11680  ennnfonelemf1  12864  resmhm2b  13396  srgfcl  13810  cnrest2  14783  lmss  14793  psmetxrge0  14879  dvfgg  15235  plyreres  15311  nninfall  16087