Definition df-f1 5203

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 5195	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5194	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4610	. . . 4 class ◡𝐹
7	6	wfun 5192	. . 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  5398  f1eq2  5399  f1eq3  5400  nff1  5401  dff12  5402  f1f  5403  f1ss  5409  f1ssr  5410  f1ssres  5412  f1cnvcnv  5414  f1co  5415  dff1o2  5447  f1f1orn  5453  f1imacnv  5459  fun11iun  5463  f11o  5475  f10  5476  f1o2ndf1  6207  ssdomg  6756  phplem4dom  6840  sbthlemi9  6942  casefun  7062  casef1  7067  djufun  7081  exmidfodomrlemim  7178  ennnfonelemf1  12373