Definition df-f 5202

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 5194	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5193	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4612	. . . 4 class ran 𝐹
7	6, 2	wss 3121	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 103	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 104	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  5330  feq2  5331  feq3  5332  nff  5344  sbcfg  5346  ffn  5347  dffn2  5349  frn  5356  dffn3  5358  fss  5359  fco  5363  funssxp  5367  fun  5370  fnfco  5372  fssres  5373  fcoi2  5379  fintm  5383  fin  5384  f0  5388  fconst  5393  f1ssr  5410  fof  5420  dff1o2  5447  fun11iun  5463  ffoss  5474  dff2  5640  fmpt  5646  ffnfv  5654  ffvresb  5659  fpr  5678  fprg  5679  idref  5736  dff1o6  5755  fliftf  5778  1stcof  6142  2ndcof  6143  smores  6271  smores2  6273  iordsmo  6276  tfrcllembfn  6336  sbthlemi9  6942  inresflem  7037  frec2uzf1od  10362  frecuzrdgtcl  10368  fclim  11257  ennnfonelemf1  12373  cnrest2  13030  lmss  13040  psmetxrge0  13126  dvfgg  13451  nninfall  14042