f1sn2g

Description: A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

		Ref	Expression
	Assertion	f1sn2g	$⊢ (A \in V \land F : \{A\} ⟶ B) \to F : \{A\} \underset{1-1}{⟶} B$

Step	Hyp	Ref	Expression
1		fsn2g	$⊢ A \in V \to (F : \{A\} ⟶ B \leftrightarrow (F (A) \in B \land F = \{⟨A, F (A)⟩\}))$
2	1	biimpa	$⊢ (A \in V \land F : \{A\} ⟶ B) \to (F (A) \in B \land F = \{⟨A, F (A)⟩\})$
3	2	simpld	$⊢ (A \in V \land F : \{A\} ⟶ B) \to F (A) \in B$
4		f1sng	$⊢ (A \in V \land F (A) \in B) \to \{⟨A, F (A)⟩\} : \{A\} \underset{1-1}{⟶} B$
5	3 4	syldan	$⊢ (A \in V \land F : \{A\} ⟶ B) \to \{⟨A, F (A)⟩\} : \{A\} \underset{1-1}{⟶} B$
6		f1eq1	$⊢ F = \{⟨A, F (A)⟩\} \to (F : \{A\} \underset{1-1}{⟶} B \leftrightarrow \{⟨A, F (A)⟩\} : \{A\} \underset{1-1}{⟶} B)$
7	2 6	simpl2im	$⊢ (A \in V \land F : \{A\} ⟶ B) \to (F : \{A\} \underset{1-1}{⟶} B \leftrightarrow \{⟨A, F (A)⟩\} : \{A\} \underset{1-1}{⟶} B)$
8	5 7	mpbird	$⊢ (A \in V \land F : \{A\} ⟶ B) \to F : \{A\} \underset{1-1}{⟶} B$

Metamath Proof Explorer