Definition df-f 5381

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 5373	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5372	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4775	. . . 4 class ran 𝐹
7	6, 2	wss 3220	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 104	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 105	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is used by:  feq1  5516  feq2  5517  feq3  5518  nff  5530  sbcfg  5532  ffn  5533  dffn2  5535  frn  5542  dffn3  5544  fss  5546  fco  5552  funssxp  5557  fun  5561  fnfco  5564  fssres  5565  fcoi2  5573  fintm  5577  fin  5578  f0  5583  fconst  5588  f1ssr  5605  fof  5615  dff1o2  5644  fun11iun  5660  ffoss  5672  dff2  5852  fmpt  5858  ffnfv  5866  ffvresb  5871  fcof  5894  fpr  5897  fprg  5898  idref  5962  dff1o6  5982  fliftf  6005  fdmrn  6034  1stcof  6397  2ndcof  6398  smores  6563  smores2  6565  iordsmo  6568  tfrcllembfn  6628  sbthlemi9  7282  inresflem  7401  frec2uzf1od  10858  frecuzrdgtcl  10864  fclim  12079  ennnfonelemf1  13361  resmhm2b  13849  srgfcl  14361  psrbaglefifi  15147  cnrest2  15428  lmss  15438  psmetxrge0  15524  dvfgg  15880  plyreres  15956  ausgrusgrben  16575  ausgrumgrien  16577  subuhgr  16679  subupgr  16680  subumgr  16681  subusgr  16682  nninfall  17218