Definition df-f1 5331

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 5323	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5322	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4724	. . . 4 class ◡𝐹
7	6	wfun 5320	. . 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  5537  f1eq2  5538  f1eq3  5539  nff1  5540  dff12  5541  f1f  5542  f1ss  5548  f1ssr  5549  f1ssres  5551  f1cnvcnv  5553  f1co  5554  dff1o2  5588  f1f1orn  5594  f1imacnv  5600  fun11iun  5604  f11o  5617  f10  5618  f1o2ndf1  6392  ssdomg  6951  phplem4dom  7047  sbthlemi9  7163  casefun  7283  casef1  7288  djufun  7302  exmidfodomrlemim  7411  4sqlemffi  12968  ennnfonelemf1  13038  usgrislfuspgrdom  16040  subusgr  16125  trlf1  16238  trlres  16240