Theorem 0xp 5724

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 4273	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 776	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 198	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1807	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1807	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5647	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 198	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4289	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4268  ⟨cop 4568   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-nul 4269  df-opab 5142  df-xp 5631

This theorem is referenced by:  dmxpid  5879  csbres  5941  res0  5942  xp0OLD  6116  xpnz  6117  xpdisj1  6119  difxp2  6124  xpcan2  6135  xpima  6140  unixp  6240  unixpid  6242  xpcoid  6248  fodomr  9063  fodomfir  9235  iundom2g  10460  indconst0  12169  indconst1  12170  hashxplem  14393  dmtrclfv  14978  ramcl  16998  0subcat  17803  mat0dimbas0  22456  mavmul0g  22543  txindislem  23623  txhaus  23637  tmdgsum  24085  ust0  24210  ehl0  25409  mbf0  25626  fconst7v  32719  hashxpe  32906  gsumpart  33151  erlval  33346  fracbas  33396  0mplrim  33705  vieta  33771  sibf0  34525  lpadlem3  34869  mexval2  35738  poimirlem5  37999  poimirlem10  38004  poimirlem22  38016  poimirlem23  38017  poimirlem26  38020  poimirlem28  38022  0fno  43886  0heALT  44234  dmrnxp  49334  0funcg2  49581  0funcALT  49585