Definition df-f1 5362

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 5354	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5353	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4753	. . . 4 class ◡𝐹
7	6	wfun 5351	. . 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  5573  f1eq2  5574  f1eq3  5575  nff1  5576  dff12  5577  f1f  5578  f1ss  5584  f1ssr  5585  f1ssres  5587  f1cnvcnv  5589  f1co  5590  dff1o2  5624  f1f1orn  5630  f1imacnv  5636  fun11iun  5640  f11o  5653  f10  5654  rinvf1o  6008  f1o2ndf1  6437  ssdomg  7031  phplem4dom  7129  sbthlemi9  7248  fsuppcorn  7267  casefun  7389  casef1  7394  djufun  7408  exmidfodomrlemim  7517  4sqlemffi  13122  ennnfonelemf1  13256  usgrislfuspgrdom  16314  subusgr  16399  trlf1  16512  trlres  16514