Definition df-f1 5136

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 5128	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5127	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4546	. . . 4 class ◡𝐹
7	6	wfun 5125	. . 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  5331  f1eq2  5332  f1eq3  5333  nff1  5334  dff12  5335  f1f  5336  f1ss  5342  f1ssr  5343  f1ssres  5345  f1cnvcnv  5347  f1co  5348  dff1o2  5380  f1f1orn  5386  f1imacnv  5392  fun11iun  5396  f11o  5408  f10  5409  f1o2ndf1  6133  ssdomg  6680  phplem4dom  6764  sbthlemi9  6861  casefun  6978  casef1  6983  djufun  6997  exmidfodomrlemim  7074  ennnfonelemf1  11967