Theorem 0xp 5750

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-nul 4280  df-opab 5168  df-xp 5657

This theorem is used by:  dmxpid  5912  csbres  5973  res0  5974  xp0OLD  6149  xpnz  6150  xpdisj1  6152  difxp2  6157  xpcan2  6169  xpima  6174  unixp  6284  unixpid  6286  xpcoid  6292  fodomr  9140  fodomfir  9312  iundom2g  10617  indconst0  12325  indconst1  12326  hashxplem  14571  dmtrclfv  15164  ramcl  17200  0subcat  18006  mat0dimbas0  22774  mavmul0g  22861  txindislem  23945  txhaus  23959  tmdgsum  24407  ust0  24532  ehl0  25731  mbf0  25948  fconst7v  33207  hashxpe  33392  gsumpart  33617  erlval  33812  fracbas  33860  0mplrim  34139  vieta  34205  sibf0  34959  lpadlem3  35303  mexval2  36247  poimirlem5  38523  poimirlem10  38528  poimirlem22  38540  poimirlem23  38541  poimirlem26  38544  poimirlem28  38546  0fno  44420  0heALT  44768  dmrnxp  49916  0funcg2  50161  0funcALT  50165