This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funsng

Description: A singleton of an ordered pair is a function. Theorem 10.5 of Quine p. 65. (Contributed by NM, 28-Jun-2011)

		Ref	Expression
	Assertion	funsng	$⊢ (A \in V \land B \in W) \to Fun \{⟨A, B⟩\}$

Step	Hyp	Ref	Expression
1		funcnvsn	$⊢ Fun {\{⟨B, A⟩\}}^{-1}$
2		cnvsng	$⊢ (B \in W \land A \in V) \to {\{⟨B, A⟩\}}^{-1} = \{⟨A, B⟩\}$
3	2	ancoms	$⊢ (A \in V \land B \in W) \to {\{⟨B, A⟩\}}^{-1} = \{⟨A, B⟩\}$
4	3	funeqd	$⊢ (A \in V \land B \in W) \to (Fun {\{⟨B, A⟩\}}^{-1} \leftrightarrow Fun \{⟨A, B⟩\})$
5	1 4	mpbii	$⊢ (A \in V \land B \in W) \to Fun \{⟨A, B⟩\}$