Theorem 0xp 5685

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.)

Assertion

Ref	Expression
0xp	⊢ (∅ × 𝐴) = ∅

Proof of Theorem 0xp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∅c0 4256  ⟨cop 4567   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595

This theorem is referenced by:  dmxpid  5839  csbres  5894  res0  5895  xp0  6061  xpnz  6062  xpdisj1  6064  difxp2  6069  xpcan2  6080  xpima  6085  unixp  6185  unixpid  6187  xpcoid  6193  fodomr  8915  xpfi  9085  iundom2g  10296  hashxplem  14148  dmtrclfv  14729  ramcl  16730  0subcat  17553  mat0dimbas0  21615  mavmul0g  21702  txindislem  22784  txhaus  22798  tmdgsum  23246  ust0  23371  ehl0  24581  mbf0  24798  hashxpe  31127  gsumpart  31315  sibf0  32301  lpadlem3  32658  mexval2  33465  poimirlem5  35782  poimirlem10  35787  poimirlem22  35799  poimirlem23  35800  poimirlem26  35803  poimirlem28  35805  0heALT  41391