Definition df-f 5384

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 5376	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5375	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4777	. . . 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  5519  feq2  5520  feq3  5521  nff  5533  sbcfg  5535  ffn  5536  dffn2  5538  frn  5545  dffn3  5547  fss  5549  fco  5555  funssxp  5560  fun  5564  fnfco  5567  fssres  5568  fcoi2  5576  fintm  5580  fin  5581  f0  5586  fconst  5591  f1ssr  5608  fof  5618  dff1o2  5647  fun11iun  5663  ffoss  5675  dff2  5855  fmpt  5861  ffnfv  5869  ffvresb  5874  fcof  5897  fpr  5900  fprg  5901  idref  5965  dff1o6  5985  fliftf  6008  fdmrn  6037  1stcof  6401  2ndcof  6402  smores  6568  smores2  6570  iordsmo  6573  tfrcllembfn  6633  sbthlemi9  7289  inresflem  7406  frec2uzf1od  10863  frecuzrdgtcl  10869  fclim  12084  ennnfonelemf1  13366  resmhm2b  13854  srgfcl  14383  psrbaglefifi  15175  cnrest2  15479  lmss  15489  psmetxrge0  15575  dvfgg  15931  plyreres  16007  ausgrusgrben  16631  ausgrumgrien  16633  subuhgr  16735  subupgr  16736  subumgr  16737  subusgr  16738  nninfall  17275