Definition df-f1 5329

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 5321	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5320	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4722	. . . 4 class ◡𝐹
7	6	wfun 5318	. . 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  5534  f1eq2  5535  f1eq3  5536  nff1  5537  dff12  5538  f1f  5539  f1ss  5545  f1ssr  5546  f1ssres  5548  f1cnvcnv  5550  f1co  5551  dff1o2  5585  f1f1orn  5591  f1imacnv  5597  fun11iun  5601  f11o  5613  f10  5614  f1o2ndf1  6388  ssdomg  6947  phplem4dom  7043  sbthlemi9  7155  casefun  7275  casef1  7280  djufun  7294  exmidfodomrlemim  7402  4sqlemffi  12959  ennnfonelemf1  13029  usgrislfuspgrdom  16029  trlf1  16183  trlres  16185