Theorem 0xp 5762

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

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4287  ⟨cop 4596   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-nul 4288  df-opab 5175  df-xp 5669

This theorem is referenced by:  dmxpid  5922  csbres  5983  res0  5984  xp0OLD  6157  xpnz  6158  xpdisj1  6160  difxp2  6165  xpcan2  6177  xpima  6182  unixp  6285  unixpid  6287  xpcoid  6293  fodomr  9117  fodomfir  9288  iundom2g  10525  indconst0  12231  indconst1  12232  hashxplem  14472  dmtrclfv  15057  ramcl  17090  0subcat  17896  mat0dimbas0  22604  mavmul0g  22691  txindislem  23771  txhaus  23785  tmdgsum  24233  ust0  24358  ehl0  25557  mbf0  25774  fconst7v  32946  hashxpe  33133  gsumpart  33364  erlval  33559  fracbas  33607  0mplrim  33885  vieta  33951  sibf0  34705  lpadlem3  35049  mexval2  35976  poimirlem5  38257  poimirlem10  38262  poimirlem22  38274  poimirlem23  38275  poimirlem26  38278  poimirlem28  38280  0fno  44144  0heALT  44492  dmrnxp  49598  0funcg2  49845  0funcALT  49849