Definition df-f 5322

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 5314	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5313	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4720	. . . 4 class ran 𝐹
7	6, 2	wss 3197	. . 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  5456  feq2  5457  feq3  5458  nff  5470  sbcfg  5472  ffn  5473  dffn2  5475  frn  5482  dffn3  5484  fss  5485  fco  5491  funssxp  5495  fun  5499  fnfco  5502  fssres  5503  fcoi2  5509  fintm  5513  fin  5514  f0  5518  fconst  5523  f1ssr  5540  fof  5550  dff1o2  5579  fun11iun  5595  ffoss  5606  dff2  5781  fmpt  5787  ffnfv  5795  ffvresb  5800  fcof  5822  fpr  5825  fprg  5826  idref  5886  dff1o6  5906  fliftf  5929  1stcof  6315  2ndcof  6316  smores  6444  smores2  6446  iordsmo  6449  tfrcllembfn  6509  sbthlemi9  7143  inresflem  7238  frec2uzf1od  10640  frecuzrdgtcl  10646  fclim  11820  ennnfonelemf1  13004  resmhm2b  13537  srgfcl  13951  cnrest2  14925  lmss  14935  psmetxrge0  15021  dvfgg  15377  plyreres  15453  ausgrusgrben  15981  ausgrumgrien  15983  nninfall  16435