Theorem 0xp 5730

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4273  ⟨cop 4573   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-nul 4274  df-opab 5148  df-xp 5637

This theorem is referenced by:  dmxpid  5885  csbres  5947  res0  5948  xp0OLD  6122  xpnz  6123  xpdisj1  6125  difxp2  6130  xpcan2  6141  xpima  6146  unixp  6246  unixpid  6248  xpcoid  6254  fodomr  9066  fodomfir  9238  iundom2g  10462  indconst0  12171  indconst1  12172  hashxplem  14395  dmtrclfv  14980  ramcl  17000  0subcat  17805  mat0dimbas0  22431  mavmul0g  22518  txindislem  23598  txhaus  23612  tmdgsum  24060  ust0  24185  ehl0  25384  mbf0  25601  fconst7v  32693  hashxpe  32880  gsumpart  33124  erlval  33319  fracbas  33366  vieta  33724  sibf0  34478  lpadlem3  34822  mexval2  35685  poimirlem5  37946  poimirlem10  37951  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem28  37969  0fno  43862  0heALT  44210  dmrnxp  49312  0funcg2  49559  0funcALT  49563