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  6393  ssdomg  6952  phplem4dom  7048  sbthlemi9  7164  casefun  7284  casef1  7289  djufun  7303  exmidfodomrlemim  7412  4sqlemffi  12987  ennnfonelemf1  13057  usgrislfuspgrdom  16060  subusgr  16145  trlf1  16258  trlres  16260