Definition df-f 5135

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 5127	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5126	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4548	. . . 4 class ran 𝐹
7	6, 2	wss 3076	. . 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  5263  feq2  5264  feq3  5265  nff  5277  sbcfg  5279  ffn  5280  dffn2  5282  frn  5289  dffn3  5291  fss  5292  fco  5296  funssxp  5300  fun  5303  fnfco  5305  fssres  5306  fcoi2  5312  fintm  5316  fin  5317  f0  5321  fconst  5326  f1ssr  5343  fof  5353  dff1o2  5380  fun11iun  5396  ffoss  5407  dff2  5572  fmpt  5578  ffnfv  5586  ffvresb  5591  fpr  5610  fprg  5611  idref  5666  dff1o6  5685  fliftf  5708  1stcof  6069  2ndcof  6070  smores  6197  smores2  6199  iordsmo  6202  tfrcllembfn  6262  sbthlemi9  6861  inresflem  6953  frec2uzf1od  10210  frecuzrdgtcl  10216  fclim  11095  ennnfonelemf1  11967  cnrest2  12444  lmss  12454  psmetxrge0  12540  dvfgg  12865  nninfall  13379