Theorem 0xp 5740

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4299  ⟨cop 4598   × cxp 5639

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-xp 5647

This theorem is referenced by:  dmxpid  5897  csbres  5956  res0  5957  xp0  6134  xpnz  6135  xpdisj1  6137  difxp2  6142  xpcan2  6153  xpima  6158  unixp  6258  unixpid  6260  xpcoid  6266  fodomr  9098  xpfiOLD  9277  fodomfir  9286  iundom2g  10500  hashxplem  14405  dmtrclfv  14991  ramcl  17007  0subcat  17807  mat0dimbas0  22360  mavmul0g  22447  txindislem  23527  txhaus  23541  tmdgsum  23989  ust0  24114  ehl0  25324  mbf0  25542  hashxpe  32739  gsumpart  33004  erlval  33216  fracbas  33262  sibf0  34332  lpadlem3  34676  mexval2  35497  poimirlem5  37626  poimirlem10  37631  poimirlem22  37643  poimirlem23  37644  poimirlem26  37647  poimirlem28  37649  0no  43431  0heALT  43779  dmrnxp  48829  0funcg2  49077  0funcALT  49081