Theorem 0xp 5762

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∅c0 4286  ⟨cop 4597   × cxp 5661

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-nul 4287  df-opab 5176  df-xp 5669

This theorem is used by:  dmxpid  5922  csbres  5983  res0  5984  xp0OLD  6157  xpnz  6158  xpdisj1  6160  difxp2  6165  xpcan2  6177  xpima  6182  unixp  6287  unixpid  6289  xpcoid  6295  fodomr  9119  fodomfir  9290  iundom2g  10535  indconst0  12241  indconst1  12242  hashxplem  14483  dmtrclfv  15074  ramcl  17106  0subcat  17912  mat0dimbas0  22652  mavmul0g  22739  txindislem  23819  txhaus  23833  tmdgsum  24281  ust0  24406  ehl0  25605  mbf0  25822  fconst7v  32994  hashxpe  33181  gsumpart  33406  erlval  33601  fracbas  33649  0mplrim  33927  vieta  33993  sibf0  34748  lpadlem3  35092  mexval2  36008  poimirlem5  38309  poimirlem10  38314  poimirlem22  38326  poimirlem23  38327  poimirlem26  38330  poimirlem28  38332  0fno  44194  0heALT  44542  dmrnxp  49648  0funcg2  49895  0funcALT  49899