Definition df-f1 5323

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 5315	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5314	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4718	. . . 4 class ◡𝐹
7	6	wfun 5312	. . 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  5528  f1eq2  5529  f1eq3  5530  nff1  5531  dff12  5532  f1f  5533  f1ss  5539  f1ssr  5540  f1ssres  5542  f1cnvcnv  5544  f1co  5545  dff1o2  5579  f1f1orn  5585  f1imacnv  5591  fun11iun  5595  f11o  5607  f10  5608  f1o2ndf1  6380  ssdomg  6938  phplem4dom  7031  sbthlemi9  7143  casefun  7263  casef1  7268  djufun  7282  exmidfodomrlemim  7390  4sqlemffi  12934  ennnfonelemf1  13004  usgrislfuspgrdom  16003  trlf1  16126  trlres  16128