Definition df-f1 5380

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 5372	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5371	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4771	. . . 4 class ◡𝐹
7	6	wfun 5369	. . 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  5591  f1eq2  5592  f1eq3  5593  nff1  5594  dff12  5595  f1f  5596  f1ss  5602  f1ssr  5603  f1ssres  5605  f1cnvcnv  5607  f1co  5608  dff1o2  5642  f1f1orn  5648  f1imacnv  5654  fun11iun  5658  f11o  5671  f10  5672  rinvf1o  6028  f1o2ndf1  6457  f1setexg  6944  ssdomg  7058  phplem4dom  7156  sbthlemi9  7275  fsuppcorn  7294  casefun  7418  casef1  7423  djufun  7437  exmidfodomrlemim  7546  4sqlemffi  13156  ennnfonelemf1  13290  usgrislfuspgrdom  16348  subusgr  16433  trlf1  16546  trlres  16548