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	⊢ ( ∅ × 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑥 ∈ ∅
2		simprl	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ∅ )
3	1 2	mto	⊢ ¬ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴 ) )
4	3	nex	⊢ ¬ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴 ) )
5	4	nex	⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴 ) )
6		elxp	⊢ ( 𝑧 ∈ ( ∅ × 𝐴 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴 ) ) )
7	5 6	mtbir	⊢ ¬ 𝑧 ∈ ( ∅ × 𝐴 )
8	7	nel0	⊢ ( ∅ × 𝐴 ) = ∅