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  5832  fpr  5835  fprg  5836  idref  5896  dff1o6  5916  fliftf  5939  1stcof  6325  2ndcof  6326  smores  6457  smores2  6459  iordsmo  6462  tfrcllembfn  6522  sbthlemi9  7163  inresflem  7258  frec2uzf1od  10667  frecuzrdgtcl  10673  fclim  11854  ennnfonelemf1  13038  resmhm2b  13571  srgfcl  13985  cnrest2  14959  lmss  14969  psmetxrge0  15055  dvfgg  15411  plyreres  15487  ausgrusgrben  16018  ausgrumgrien  16020  subuhgr  16122  subupgr  16123  subumgr  16124  subusgr  16125  nninfall  16611