Definition df-f1 5273

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 5265	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5264	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4672	. . . 4 class ◡𝐹
7	6	wfun 5262	. . 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  5470  f1eq2  5471  f1eq3  5472  nff1  5473  dff12  5474  f1f  5475  f1ss  5481  f1ssr  5482  f1ssres  5484  f1cnvcnv  5486  f1co  5487  dff1o2  5521  f1f1orn  5527  f1imacnv  5533  fun11iun  5537  f11o  5549  f10  5550  f1o2ndf1  6304  ssdomg  6855  phplem4dom  6941  sbthlemi9  7049  casefun  7169  casef1  7174  djufun  7188  exmidfodomrlemim  7291  4sqlemffi  12638  ennnfonelemf1  12708