Definition df-f 5361

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 5353	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5352	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4755	. . . 4 class ran 𝐹
7	6, 2	wss 3214	. . 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  5496  feq2  5497  feq3  5498  nff  5510  sbcfg  5512  ffn  5513  dffn2  5515  frn  5522  dffn3  5524  fss  5526  fco  5532  funssxp  5537  fun  5541  fnfco  5544  fssres  5545  fcoi2  5553  fintm  5557  fin  5558  f0  5563  fconst  5568  f1ssr  5585  fof  5595  dff1o2  5624  fun11iun  5640  ffoss  5652  dff2  5826  fmpt  5832  ffnfv  5840  ffvresb  5845  fcof  5868  fpr  5871  fprg  5872  idref  5935  dff1o6  5955  fliftf  5978  fdmrn  6007  1stcof  6370  2ndcof  6371  smores  6536  smores2  6538  iordsmo  6541  tfrcllembfn  6601  sbthlemi9  7248  inresflem  7364  frec2uzf1od  10792  frecuzrdgtcl  10798  fclim  12004  ennnfonelemf1  13253  resmhm2b  13744  srgfcl  14216  cnrest2  15227  lmss  15237  psmetxrge0  15323  dvfgg  15679  plyreres  15755  ausgrusgrben  16289  ausgrumgrien  16291  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  nninfall  16913