Definition df-f 5330

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 5322	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5321	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4726	. . . 4 class ran 𝐹
7	6, 2	wss 3200	. . 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  5465  feq2  5466  feq3  5467  nff  5479  sbcfg  5481  ffn  5482  dffn2  5484  frn  5491  dffn3  5493  fss  5494  fco  5500  funssxp  5504  fun  5508  fnfco  5511  fssres  5512  fcoi2  5518  fintm  5522  fin  5523  f0  5527  fconst  5532  f1ssr  5549  fof  5559  dff1o2  5588  fun11iun  5604  ffoss  5616  dff2  5791  fmpt  5797  ffnfv  5805  ffvresb  5810  fcof  5833  fpr  5836  fprg  5837  idref  5897  dff1o6  5917  fliftf  5940  1stcof  6326  2ndcof  6327  smores  6458  smores2  6460  iordsmo  6463  tfrcllembfn  6523  sbthlemi9  7164  inresflem  7259  frec2uzf1od  10669  frecuzrdgtcl  10675  fclim  11872  ennnfonelemf1  13057  resmhm2b  13590  srgfcl  14005  cnrest2  14979  lmss  14989  psmetxrge0  15075  dvfgg  15431  plyreres  15507  ausgrusgrben  16038  ausgrumgrien  16040  subuhgr  16142  subupgr  16143  subumgr  16144  subusgr  16145  nninfall  16662