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  7400  frec2uzf1od  10843  frecuzrdgtcl  10849  fclim  12060  ennnfonelemf1  13309  resmhm2b  13796  srgfcl  14277  cnrest2  15337  lmss  15347  psmetxrge0  15433  dvfgg  15789  plyreres  15865  ausgrusgrben  16409  ausgrumgrien  16411  subuhgr  16513  subupgr  16514  subumgr  16515  subusgr  16516  nninfall  17052