Theorem 0xp 5723

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 4290	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 770	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1801	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1801	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxpi 5646	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mto 197	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4306	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4285  ⟨cop 4586   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-nul 4286  df-opab 5161  df-xp 5630

This theorem is referenced by:  dmxpid  5879  csbres  5941  res0  5942  xp0OLD  6116  xpnz  6117  xpdisj1  6119  difxp2  6124  xpcan2  6135  xpima  6140  unixp  6240  unixpid  6242  xpcoid  6248  fodomr  9056  fodomfir  9228  iundom2g  10450  hashxplem  14356  dmtrclfv  14941  ramcl  16957  0subcat  17762  mat0dimbas0  22410  mavmul0g  22497  txindislem  23577  txhaus  23591  tmdgsum  24039  ust0  24164  ehl0  25373  mbf0  25591  fconst7v  32698  hashxpe  32887  indconst0  32939  indconst1  32940  gsumpart  33146  erlval  33340  fracbas  33387  vieta  33736  sibf0  34491  lpadlem3  34835  mexval2  35697  poimirlem5  37826  poimirlem10  37831  poimirlem22  37843  poimirlem23  37844  poimirlem26  37847  poimirlem28  37849  0fno  43676  0heALT  44024  dmrnxp  49082  0funcg2  49329  0funcALT  49333