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 x A

Proof

Step Hyp Ref Expression
1 0ex V
2 1 snid
3 ixp0x x A =
4 2 3 eleqtrri x A