Theorem 0xp 5199

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 3919	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 794	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 188	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1731	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1731	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxp 5131	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mtbir 313	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 3932	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∅c0 3915  ⟨cop 4183   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120

This theorem is referenced by:  dmxpid  5345  csbres  5399  res0  5400  xp0  5552  xpnz  5553  xpdisj1  5555  difxp2  5560  xpcan2  5571  xpima  5576  unixp  5668  unixpid  5670  xpcoid  5676  fodomr  8111  xpfi  8231  cdaassen  9004  iundom2g  9362  alephadd  9399  hashxplem  13220  dmtrclfv  13759  ramcl  15733  0subcat  16498  mat0dimbas0  20272  mavmul0g  20359  txindislem  21436  txhaus  21450  tmdgsum  21899  ust0  22023  sibf0  30396  mexval2  31400  poimirlem5  33414  poimirlem10  33419  poimirlem22  33431  poimirlem23  33432  poimirlem26  33435  poimirlem28  33437  0mbf  33455  0heALT  38077