Theorem 0xp 5754

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4279  ⟨cop 4590   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-nul 4280  df-opab 5168  df-xp 5661

This theorem is used by:  dmxpid  5914  csbres  5975  res0  5976  xp0OLD  6150  xpnz  6151  xpdisj1  6153  difxp2  6158  xpcan2  6170  xpima  6175  unixp  6280  unixpid  6282  xpcoid  6288  fodomr  9126  fodomfir  9297  iundom2g  10548  indconst0  12254  indconst1  12255  hashxplem  14498  dmtrclfv  15091  ramcl  17121  0subcat  17927  mat0dimbas0  22688  mavmul0g  22775  txindislem  23859  txhaus  23873  tmdgsum  24321  ust0  24446  ehl0  25645  mbf0  25862  fconst7v  33093  hashxpe  33278  gsumpart  33503  erlval  33698  fracbas  33746  0mplrim  34024  vieta  34090  sibf0  34845  lpadlem3  35189  mexval2  36082  poimirlem5  38374  poimirlem10  38379  poimirlem22  38391  poimirlem23  38392  poimirlem26  38395  poimirlem28  38397  0fno  44275  0heALT  44623  dmrnxp  49765  0funcg2  50010  0funcALT  50014