fnsnb

Description: A function whose domain is a singleton can be represented as a singleton of an ordered pair. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) Revised to add reverse implication. (Revised by NM, 29-Dec-2018)

		Ref	Expression
	Hypothesis	fnsnb.1	$⊢ A \in V$
	Assertion	fnsnb	$⊢ F Fn \{A\} \leftrightarrow F = \{⟨A, F (A)⟩\}$

Proof

Step	Hyp	Ref	Expression
1		fnsnb.1	$⊢ A \in V$
2		fnsnr	$⊢ F Fn \{A\} \to (x \in F \to x = ⟨A, F (A)⟩)$
3		df-fn	$⊢ F Fn \{A\} \leftrightarrow (Fun F \land dom F = \{A\})$
4	1	snid	$⊢ A \in \{A\}$
5		eleq2	$⊢ dom F = \{A\} \to (A \in dom F \leftrightarrow A \in \{A\})$
6	4 5	mpbiri	$⊢ dom F = \{A\} \to A \in dom F$
7	6	anim2i	$⊢ (Fun F \land dom F = \{A\}) \to (Fun F \land A \in dom F)$
8	3 7	sylbi	$⊢ F Fn \{A\} \to (Fun F \land A \in dom F)$
9		funfvop	$⊢ (Fun F \land A \in dom F) \to ⟨A, F (A)⟩ \in F$
10	8 9	syl	$⊢ F Fn \{A\} \to ⟨A, F (A)⟩ \in F$
11		eleq1	$⊢ x = ⟨A, F (A)⟩ \to (x \in F \leftrightarrow ⟨A, F (A)⟩ \in F)$
12	10 11	syl5ibrcom	$⊢ F Fn \{A\} \to (x = ⟨A, F (A)⟩ \to x \in F)$
13	2 12	impbid	$⊢ F Fn \{A\} \to (x \in F \leftrightarrow x = ⟨A, F (A)⟩)$
14		velsn	$⊢ x \in \{⟨A, F (A)⟩\} \leftrightarrow x = ⟨A, F (A)⟩$
15	13 14	bitr4di	$⊢ F Fn \{A\} \to (x \in F \leftrightarrow x \in \{⟨A, F (A)⟩\})$
16	15	eqrdv	$⊢ F Fn \{A\} \to F = \{⟨A, F (A)⟩\}$
17		fvex	$⊢ F (A) \in V$
18	1 17	fnsn	$⊢ \{⟨A, F (A)⟩\} Fn \{A\}$
19		fneq1	$⊢ F = \{⟨A, F (A)⟩\} \to (F Fn \{A\} \leftrightarrow \{⟨A, F (A)⟩\} Fn \{A\})$
20	18 19	mpbiri	$⊢ F = \{⟨A, F (A)⟩\} \to F Fn \{A\}$
21	16 20	impbii	$⊢ F Fn \{A\} \leftrightarrow F = \{⟨A, F (A)⟩\}$

Metamath Proof Explorer

Theorem fnsnb

Proof