Theorem 0xp 5619

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 4231	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 771	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 200	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1803	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1803	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxp 5548	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mtbir 327	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4250	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∅c0 4226  ⟨cop 4529   × cxp 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-dif 3862  df-un 3864  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-opab 5096  df-xp 5531

This theorem is referenced by:  dmxpid  5772  csbres  5827  res0  5828  xp0  5988  xpnz  5989  xpdisj1  5991  difxp2  5996  xpcan2  6007  xpima  6012  unixp  6112  unixpid  6114  xpcoid  6120  fodomr  8691  xpfi  8823  iundom2g  10001  hashxplem  13845  dmtrclfv  14426  ramcl  16421  0subcat  17168  mat0dimbas0  21167  mavmul0g  21254  txindislem  22334  txhaus  22348  tmdgsum  22796  ust0  22921  ehl0  24118  mbf0  24335  hashxpe  30652  gsumpart  30842  sibf0  31821  lpadlem3  32178  mexval2  32982  poimirlem5  35343  poimirlem10  35348  poimirlem22  35360  poimirlem23  35361  poimirlem26  35364  poimirlem28  35366  0heALT  40858