Metamath Proof Explorer

Theorem 0xp

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

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

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. x e. (/)
2 simprl 
 |-  ( ( z = <. x , y >. /\ ( x e. (/) /\ y e. A ) ) -> x e. (/) )
3 1 2 mto 
 |-  -. ( z = <. x , y >. /\ ( x e. (/) /\ y e. A ) )
4 3 nex 
 |-  -. E. y ( z = <. x , y >. /\ ( x e. (/) /\ y e. A ) )
5 4 nex 
 |-  -. E. x E. y ( z = <. x , y >. /\ ( x e. (/) /\ y e. A ) )
6 elxp 
 |-  ( z e. ( (/) X. A ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. (/) /\ y e. A ) ) )
7 5 6 mtbir 
 |-  -. z e. ( (/) X. A )
8 7 nel0 
 |-  ( (/) X. A ) = (/)