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

Metamath Proof Explorer

Theorem xp0OLD

Description: Obsolete version of xp0 as of 1-Feb-2026. (Contributed by NM, 12-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	xp0OLD	$⊢ A \times \emptyset = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		0xp	$⊢ \emptyset \times A = \emptyset$
2	1	cnveqi	$⊢ {(\emptyset \times A)}^{-1} = \emptyset^{-1}$
3		cnvxp	$⊢ {(\emptyset \times A)}^{-1} = A \times \emptyset$
4		cnv0	$⊢ \emptyset^{-1} = \emptyset$
5	2 3 4	3eqtr3i	$⊢ A \times \emptyset = \emptyset$