Theorem 0xp 5758

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 4287	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 783	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 200	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1833	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1833	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5681	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 200	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4305	1 ⊢ (∅ × 𝐴) = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4282  ⟨cop 4593   × cxp 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3905  df-nul 4283  df-opab 5172  df-xp 5665

This theorem is used by:  dmxpid  5918  csbres  5979  res0  5980  xp0OLD  6154  xpnz  6155  xpdisj1  6157  difxp2  6162  xpcan2  6174  xpima  6179  unixp  6284  unixpid  6286  xpcoid  6292  fodomr  9130  fodomfir  9301  iundom2g  10552  indconst0  12258  indconst1  12259  hashxplem  14502  dmtrclfv  15095  ramcl  17127  0subcat  17933  mat0dimbas0  22694  mavmul0g  22781  txindislem  23865  txhaus  23879  tmdgsum  24327  ust0  24452  ehl0  25651  mbf0  25868  fconst7v  33101  hashxpe  33286  gsumpart  33511  erlval  33706  fracbas  33754  0mplrim  34032  vieta  34098  sibf0  34853  lpadlem3  35197  mexval2  36090  poimirlem5  38382  poimirlem10  38387  poimirlem22  38399  poimirlem23  38400  poimirlem26  38403  poimirlem28  38405  0fno  44283  0heALT  44631  dmrnxp  49773  0funcg2  50018  0funcALT  50022