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

Metamath Proof Explorer

Theorem xpsneng

Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 22-Oct-2004)

		Ref	Expression
	Assertion	xpsneng	$⊢ (A \in V \land B \in W) \to (A \times \{B\}) \approx A$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$⊢ x = A \to x \times \{y\} = A \times \{y\}$
2		id	$⊢ x = A \to x = A$
3	1 2	breq12d	$⊢ x = A \to ((x \times \{y\}) \approx x \leftrightarrow (A \times \{y\}) \approx A)$
4		sneq	$⊢ y = B \to \{y\} = \{B\}$
5	4	xpeq2d	$⊢ y = B \to A \times \{y\} = A \times \{B\}$
6	5	breq1d	$⊢ y = B \to ((A \times \{y\}) \approx A \leftrightarrow (A \times \{B\}) \approx A)$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	xpsnen	$⊢ (x \times \{y\}) \approx x$
10	3 6 9	vtocl2g	$⊢ (A \in V \land B \in W) \to (A \times \{B\}) \approx A$