Definition df-f1 5192

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 5184	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5183	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4602	. . . 4 class ◡𝐹
7	6	wfun 5181	. . 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  5387  f1eq2  5388  f1eq3  5389  nff1  5390  dff12  5391  f1f  5392  f1ss  5398  f1ssr  5399  f1ssres  5401  f1cnvcnv  5403  f1co  5404  dff1o2  5436  f1f1orn  5442  f1imacnv  5448  fun11iun  5452  f11o  5464  f10  5465  f1o2ndf1  6192  ssdomg  6740  phplem4dom  6824  sbthlemi9  6926  casefun  7046  casef1  7051  djufun  7065  exmidfodomrlemim  7153  ennnfonelemf1  12347