Theorem 0xp 5722

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 770	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1800	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1800	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxp 5646	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mtbir 323	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4307	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4286  ⟨cop 4585   × cxp 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-xp 5629

This theorem is referenced by:  dmxpid  5876  csbres  5937  res0  5938  xp0  6111  xpnz  6112  xpdisj1  6114  difxp2  6119  xpcan2  6130  xpima  6135  unixp  6234  unixpid  6236  xpcoid  6242  fodomr  9052  xpfiOLD  9228  fodomfir  9237  iundom2g  10453  hashxplem  14358  dmtrclfv  14943  ramcl  16959  0subcat  17763  mat0dimbas0  22369  mavmul0g  22456  txindislem  23536  txhaus  23550  tmdgsum  23998  ust0  24123  ehl0  25333  mbf0  25551  hashxpe  32765  gsumpart  33023  erlval  33211  fracbas  33257  sibf0  34304  lpadlem3  34648  mexval2  35478  poimirlem5  37607  poimirlem10  37612  poimirlem22  37624  poimirlem23  37625  poimirlem26  37628  poimirlem28  37630  0no  43411  0heALT  43759  dmrnxp  48825  0funcg2  49073  0funcALT  49077