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  6567  smores2  6569  iordsmo  6572  tfrcllembfn  6632  sbthlemi9  7287  inresflem  7406  frec2uzf1od  10864  frecuzrdgtcl  10870  fclim  12085  ennnfonelemf1  13367  resmhm2b  13855  srgfcl  14384  psrbaglefifi  15172  cnrest2  15462  lmss  15472  psmetxrge0  15558  dvfgg  15914  plyreres  15990  ausgrusgrben  16614  ausgrumgrien  16616  subuhgr  16718  subupgr  16719  subumgr  16720  subusgr  16721  nninfall  17258