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  10856  frecuzrdgtcl  10862  fclim  12076  ennnfonelemf1  13358  resmhm2b  13845  srgfcl  14326  cnrest2  15386  lmss  15396  psmetxrge0  15482  dvfgg  15838  plyreres  15914  ausgrusgrben  16507  ausgrumgrien  16509  subuhgr  16611  subupgr  16612  subumgr  16613  subusgr  16614  nninfall  17150