Theorem 0xp 5742

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 4288	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 780	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 199	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1819	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1819	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5665	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 199	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4304	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∅c0 4283  ⟨cop 4585   × cxp 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3905  df-nul 4284  df-opab 5160  df-xp 5649

This theorem is referenced by:  dmxpid  5902  csbres  5964  res0  5965  xp0OLD  6139  xpnz  6140  xpdisj1  6142  difxp2  6147  xpcan2  6158  xpima  6163  unixp  6264  unixpid  6266  xpcoid  6272  fodomr  9094  fodomfir  9266  iundom2g  10491  indconst0  12201  indconst1  12202  hashxplem  14440  dmtrclfv  15025  ramcl  17056  0subcat  17862  mat0dimbas0  22514  mavmul0g  22601  txindislem  23681  txhaus  23695  tmdgsum  24143  ust0  24268  ehl0  25467  mbf0  25684  fconst7v  32783  hashxpe  32970  gsumpart  33204  erlval  33400  fracbas  33453  0mplrim  33772  vieta  33838  sibf0  34592  lpadlem3  34936  mexval2  35814  poimirlem5  38085  poimirlem10  38090  poimirlem22  38102  poimirlem23  38103  poimirlem26  38106  poimirlem28  38108  0fno  43972  0heALT  44320  dmrnxp  49419  0funcg2  49666  0funcALT  49670