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

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