Theorem 0xp 5723

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 4279	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 771	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1802	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5646	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 197	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4295	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4274  ⟨cop 4574   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-nul 4275  df-opab 5149  df-xp 5630

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  9059  fodomfir  9231  iundom2g  10453  indconst0  12162  indconst1  12163  hashxplem  14386  dmtrclfv  14971  ramcl  16991  0subcat  17796  mat0dimbas0  22441  mavmul0g  22528  txindislem  23608  txhaus  23622  tmdgsum  24070  ust0  24195  ehl0  25394  mbf0  25611  fconst7v  32708  hashxpe  32895  gsumpart  33139  erlval  33334  fracbas  33381  vieta  33739  sibf0  34494  lpadlem3  34838  mexval2  35701  poimirlem5  37960  poimirlem10  37965  poimirlem22  37977  poimirlem23  37978  poimirlem26  37981  poimirlem28  37983  0fno  43880  0heALT  44228  dmrnxp  49324  0funcg2  49571  0funcALT  49575