Definition df-f 5358

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

This definition is referenced by:  feq1  5493  feq2  5494  feq3  5495  nff  5507  sbcfg  5509  ffn  5510  dffn2  5512  frn  5519  dffn3  5521  fss  5523  fco  5529  funssxp  5534  fun  5538  fnfco  5541  fssres  5542  fcoi2  5550  fintm  5554  fin  5555  f0  5560  fconst  5565  f1ssr  5582  fof  5592  dff1o2  5621  fun11iun  5637  ffoss  5649  dff2  5823  fmpt  5829  ffnfv  5837  ffvresb  5842  fcof  5865  fpr  5868  fprg  5869  idref  5931  dff1o6  5951  fliftf  5974  1stcof  6359  2ndcof  6360  smores  6525  smores2  6527  iordsmo  6530  tfrcllembfn  6590  sbthlemi9  7237  inresflem  7353  frec2uzf1od  10772  frecuzrdgtcl  10778  fclim  11983  ennnfonelemf1  13186  resmhm2b  13719  srgfcl  14134  cnrest2  15118  lmss  15128  psmetxrge0  15214  dvfgg  15570  plyreres  15646  ausgrusgrben  16180  ausgrumgrien  16182  subuhgr  16284  subupgr  16285  subumgr  16286  subusgr  16287  nninfall  16804