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

Syntax hints:   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∅c0 4294  ⟨cop 4597   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-nul 4295  df-opab 5175  df-xp 5665

This theorem is referenced by:  dmxpid  5918  csbres  5979  res0  5980  xp0OLD  6154  xpnz  6155  xpdisj1  6157  difxp2  6162  xpcan2  6174  xpima  6179  unixp  6280  unixpid  6282  xpcoid  6288  fodomr  9112  fodomfir  9283  iundom2g  10520  indconst0  12226  indconst1  12227  hashxplem  14466  dmtrclfv  15051  ramcl  17085  0subcat  17891  mat0dimbas0  22588  mavmul0g  22675  txindislem  23755  txhaus  23769  tmdgsum  24217  ust0  24342  ehl0  25541  mbf0  25758  fconst7v  32902  hashxpe  33089  gsumpart  33320  erlval  33515  fracbas  33565  0mplrim  33845  vieta  33911  sibf0  34665  lpadlem3  35009  mexval2  35890  poimirlem5  38159  poimirlem10  38164  poimirlem22  38176  poimirlem23  38177  poimirlem26  38180  poimirlem28  38182  0fno  44046  0heALT  44394  dmrnxp  49493  0funcg2  49740  0funcALT  49744