Definition df-f 5222

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 5214	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 5213	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 4629	. . . 4 class ran 𝐹
7	6, 2	wss 3131	. . 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  5350  feq2  5351  feq3  5352  nff  5364  sbcfg  5366  ffn  5367  dffn2  5369  frn  5376  dffn3  5378  fss  5379  fco  5383  funssxp  5387  fun  5390  fnfco  5392  fssres  5393  fcoi2  5399  fintm  5403  fin  5404  f0  5408  fconst  5413  f1ssr  5430  fof  5440  dff1o2  5468  fun11iun  5484  ffoss  5495  dff2  5662  fmpt  5668  ffnfv  5676  ffvresb  5681  fpr  5700  fprg  5701  idref  5759  dff1o6  5779  fliftf  5802  1stcof  6166  2ndcof  6167  smores  6295  smores2  6297  iordsmo  6300  tfrcllembfn  6360  sbthlemi9  6966  inresflem  7061  frec2uzf1od  10408  frecuzrdgtcl  10414  fclim  11304  ennnfonelemf1  12421  srgfcl  13161  cnrest2  13821  lmss  13831  psmetxrge0  13917  dvfgg  14242  nninfall  14843