Definition df-f1 5128

Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1 5120	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5119	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4538	. . . 4 class ◡𝐹
7	6	wfun 5117	. . 3 wff Fun ◡𝐹
8	5, 7	wa 103	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 104	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5323  f1eq2  5324  f1eq3  5325  nff1  5326  dff12  5327  f1f  5328  f1ss  5334  f1ssr  5335  f1ssres  5337  f1cnvcnv  5339  f1co  5340  dff1o2  5372  f1f1orn  5378  f1imacnv  5384  fun11iun  5388  f11o  5400  f10  5401  f1o2ndf1  6125  ssdomg  6672  phplem4dom  6756  sbthlemi9  6853  casefun  6970  casef1  6975  djufun  6989  exmidfodomrlemim  7057  ennnfonelemf1  11931