Theorem 0xp 5715

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 770	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1801	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1801	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxp 5639	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mtbir 323	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4304	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∅c0 4283  ⟨cop 4582   × cxp 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-xp 5622

This theorem is referenced by:  dmxpid  5870  csbres  5931  res0  5932  xp0  6105  xpnz  6106  xpdisj1  6108  difxp2  6113  xpcan2  6124  xpima  6129  unixp  6229  unixpid  6231  xpcoid  6237  fodomr  9041  fodomfir  9212  iundom2g  10431  hashxplem  14340  dmtrclfv  14925  ramcl  16941  0subcat  17745  mat0dimbas0  22382  mavmul0g  22469  txindislem  23549  txhaus  23563  tmdgsum  24011  ust0  24136  ehl0  25345  mbf0  25563  fconst7v  32601  hashxpe  32787  gsumpart  33035  erlval  33223  fracbas  33269  sibf0  34345  lpadlem3  34689  mexval2  35545  poimirlem5  37671  poimirlem10  37676  poimirlem22  37688  poimirlem23  37689  poimirlem26  37692  poimirlem28  37694  0no  43474  0heALT  43822  dmrnxp  48874  0funcg2  49122  0funcALT  49126