Definition df-f1 5338

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 5330	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5329	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4730	. . . 4 class ◡𝐹
7	6	wfun 5327	. . 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  5546  f1eq2  5547  f1eq3  5548  nff1  5549  dff12  5550  f1f  5551  f1ss  5557  f1ssr  5558  f1ssres  5560  f1cnvcnv  5562  f1co  5563  dff1o2  5597  f1f1orn  5603  f1imacnv  5609  fun11iun  5613  f11o  5626  f10  5627  f1o2ndf1  6402  ssdomg  6995  phplem4dom  7091  sbthlemi9  7207  fsuppcorn  7226  casefun  7344  casef1  7349  djufun  7363  exmidfodomrlemim  7472  4sqlemffi  13049  ennnfonelemf1  13119  usgrislfuspgrdom  16131  subusgr  16216  trlf1  16329  trlres  16331