Let $X$ and $Y$ each be a D11: Set.
The set of bijections from $X$ to $Y$ is the D11: Set
\begin{equation}
\text{Bij}(X \to Y) : = \{ f \mid f : X \to Y \text{ is a bijection} \}
\end{equation}
▼  Set of symbols 
▼  Alphabet 
▼  Deduction system 
▼  Theory 
▼  ZermeloFraenkel set theory 
▼  Set 
▼  Binary cartesian set product 
▼  Binary relation 
▼  Map 
▼  Bijective map 
▶  Countable set 
▶  Isomorphic sets 
▶ 
Convention 0
(Notation for set of bijections)
Let $X$ and $Y$ each be a D11: Set. We denote the D2221: Set of bijections from $X$ to $Y$ by $\text{Bij}(X \to Y)$.
