Theorem 0nelxp

Description: The empty set is not a member of a Cartesian product. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 26-Apr-2015) (Proof shortened by JJ, 13-Aug-2021)

	Ref	Expression
Assertion	0nelxp	⊢ ¬ ∅ ∈ ( 𝐴 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opnzi	⊢ ⟨ 𝑥 , 𝑦 ⟩ ≠ ∅
4	3	nesymi	⊢ ¬ ∅ = ⟨ 𝑥 , 𝑦 ⟩
5	4	intnanr	⊢ ¬ ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
6	5	nex	⊢ ¬ ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
7	6	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
8		elxp	⊢ ( ∅ ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
9	7 8	mtbir	⊢ ¬ ∅ ∈ ( 𝐴 × 𝐵 )