Metamath Proof Explorer

Theorem xp0

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004)

Ref Expression
Assertion xp0 
|- ( A X. (/) ) = (/)

Proof

Step Hyp Ref Expression
1 0xp 
 |-  ( (/) X. A ) = (/)
2 1 cnveqi 
 |-  `' ( (/) X. A ) = `' (/)
3 cnvxp 
 |-  `' ( (/) X. A ) = ( A X. (/) )
4 cnv0 
 |-  `' (/) = (/)
5 2 3 4 3eqtr3i 
 |-  ( A X. (/) ) = (/)