Definition df-f1 5322

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 5314	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5313	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4717	. . . 4 class ◡𝐹
7	6	wfun 5311	. . 3 wff Fun ◡𝐹
8	5, 7	wa 104	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 105	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5525  f1eq2  5526  f1eq3  5527  nff1  5528  dff12  5529  f1f  5530  f1ss  5536  f1ssr  5537  f1ssres  5539  f1cnvcnv  5541  f1co  5542  dff1o2  5576  f1f1orn  5582  f1imacnv  5588  fun11iun  5592  f11o  5604  f10  5605  f1o2ndf1  6372  ssdomg  6928  phplem4dom  7019  sbthlemi9  7128  casefun  7248  casef1  7253  djufun  7267  exmidfodomrlemim  7375  4sqlemffi  12914  ennnfonelemf1  12984  usgrislfuspgrdom  15982