Metamath Proof Explorer

Theorem 0elixp

Description: Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006)

Ref Expression
Assertion 0elixp 
|- (/) e. X_ x e. (/) A

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 snid 
 |-  (/) e. { (/) }
3 ixp0x 
 |-  X_ x e. (/) A = { (/) }
4 2 3 eleqtrri 
 |-  (/) e. X_ x e. (/) A