Theorem 0xp 5731

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 4292	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 771	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1802	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5654	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 197	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4308	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4287  ⟨cop 4588   × cxp 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-nul 4288  df-opab 5163  df-xp 5638

This theorem is referenced by:  dmxpid  5887  csbres  5949  res0  5950  xp0OLD  6124  xpnz  6125  xpdisj1  6127  difxp2  6132  xpcan2  6143  xpima  6148  unixp  6248  unixpid  6250  xpcoid  6256  fodomr  9068  fodomfir  9240  iundom2g  10462  hashxplem  14368  dmtrclfv  14953  ramcl  16969  0subcat  17774  mat0dimbas0  22422  mavmul0g  22509  txindislem  23589  txhaus  23603  tmdgsum  24051  ust0  24176  ehl0  25385  mbf0  25603  fconst7v  32709  hashxpe  32897  indconst0  32949  indconst1  32950  gsumpart  33156  erlval  33351  fracbas  33398  vieta  33756  sibf0  34511  lpadlem3  34855  mexval2  35716  poimirlem5  37873  poimirlem10  37878  poimirlem22  37890  poimirlem23  37891  poimirlem26  37894  poimirlem28  37896  0fno  43788  0heALT  44136  dmrnxp  49193  0funcg2  49440  0funcALT  49444