fnsnr

Description: If a class belongs to a function on a singleton, then that class is the obvious ordered pair. Note that this theorem also holds when A is a proper class, but its meaning is then different. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016)

		Ref	Expression
	Assertion	fnsnr	$⊢ F Fn \{A\} \to (B \in F \to B = ⟨A, F (A)⟩)$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$⊢ F Fn \{A\} \to {F ↾}_{\{A\}} = F$
2		fnfun	$⊢ F Fn \{A\} \to Fun F$
3		funressn	$⊢ Fun F \to {F ↾}_{\{A\}} \subseteq \{⟨A, F (A)⟩\}$
4	2 3	syl	$⊢ F Fn \{A\} \to {F ↾}_{\{A\}} \subseteq \{⟨A, F (A)⟩\}$
5	1 4	eqsstrrd	$⊢ F Fn \{A\} \to F \subseteq \{⟨A, F (A)⟩\}$
6	5	sseld	$⊢ F Fn \{A\} \to (B \in F \to B \in \{⟨A, F (A)⟩\})$
7		elsni	$⊢ B \in \{⟨A, F (A)⟩\} \to B = ⟨A, F (A)⟩$
8	6 7	syl6	$⊢ F Fn \{A\} \to (B \in F \to B = ⟨A, F (A)⟩)$

Metamath Proof Explorer

Theorem fnsnr

Proof