Theorem 0xp 5724

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4286  ⟨cop 4587   × cxp 5623

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-dif 3905  df-nul 4287  df-opab 5162  df-xp 5631

This theorem is referenced by:  dmxpid  5880  csbres  5942  res0  5943  xp0OLD  6117  xpnz  6118  xpdisj1  6120  difxp2  6125  xpcan2  6136  xpima  6141  unixp  6241  unixpid  6243  xpcoid  6249  fodomr  9060  fodomfir  9232  iundom2g  10454  hashxplem  14360  dmtrclfv  14945  ramcl  16961  0subcat  17766  mat0dimbas0  22414  mavmul0g  22501  txindislem  23581  txhaus  23595  tmdgsum  24043  ust0  24168  ehl0  25377  mbf0  25595  fconst7v  32680  hashxpe  32868  indconst0  32920  indconst1  32921  gsumpart  33127  erlval  33321  fracbas  33368  vieta  33717  sibf0  34472  lpadlem3  34816  mexval2  35678  poimirlem5  37797  poimirlem10  37802  poimirlem22  37814  poimirlem23  37815  poimirlem26  37818  poimirlem28  37820  0no  43712  0heALT  44060  dmrnxp  49118  0funcg2  49365  0funcALT  49369