Definition df-f 5328

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 5320	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5319	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4724	. . . 4 class ran 𝐹
7	6, 2	wss 3198	. . 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  5462  feq2  5463  feq3  5464  nff  5476  sbcfg  5478  ffn  5479  dffn2  5481  frn  5488  dffn3  5490  fss  5491  fco  5497  funssxp  5501  fun  5505  fnfco  5508  fssres  5509  fcoi2  5515  fintm  5519  fin  5520  f0  5524  fconst  5529  f1ssr  5546  fof  5556  dff1o2  5585  fun11iun  5601  ffoss  5612  dff2  5787  fmpt  5793  ffnfv  5801  ffvresb  5806  fcof  5828  fpr  5831  fprg  5832  idref  5892  dff1o6  5912  fliftf  5935  1stcof  6321  2ndcof  6322  smores  6453  smores2  6455  iordsmo  6458  tfrcllembfn  6518  sbthlemi9  7155  inresflem  7250  frec2uzf1od  10658  frecuzrdgtcl  10664  fclim  11845  ennnfonelemf1  13029  resmhm2b  13562  srgfcl  13976  cnrest2  14950  lmss  14960  psmetxrge0  15046  dvfgg  15402  plyreres  15478  ausgrusgrben  16007  ausgrumgrien  16009  nninfall  16547