Theorem 0xp 5749

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4278  ⟨cop 4834   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 4047  df-nul 4279  df-opab 5167  df-xp 5656

This theorem is used by:  dmxpid  5911  csbres  5972  res0  5973  xp0OLD  6148  xpnz  6149  xpdisj1  6151  difxp2  6156  xpcan2  6168  xpima  6173  unixp  6285  unixpid  6287  xpcoid  6293  fodomr  9151  fodomfir  9323  iundom2g  10628  indconst0  12336  indconst1  12337  hashxplem  14582  dmtrclfv  15177  ramcl  17213  0subcat  18019  mat0dimbas0  22787  mavmul0g  22874  txindislem  23958  txhaus  23972  tmdgsum  24420  ust0  24545  ehl0  25744  mbf0  25961  fconst7v  33262  hashxpe  33446  gsumpart  33671  erlval  33866  fracbas  33914  0mplrim  34193  vieta  34259  sibf0  35013  lpadlem3  35357  mexval2  36355  poimirlem5  38637  poimirlem10  38642  poimirlem22  38654  poimirlem23  38655  poimirlem26  38658  poimirlem28  38660  0fno  44530  0heALT  44877  dmrnxp  50042  0funcg2  50293  0funcALT  50297