Theorem 0xp 5782

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

Syntax hints:   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∅c0 4332  ⟨cop 4630   × cxp 5681

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-opab 5204  df-xp 5689

This theorem is referenced by:  dmxpid  5939  csbres  5998  res0  5999  xp0  6176  xpnz  6177  xpdisj1  6179  difxp2  6184  xpcan2  6195  xpima  6200  unixp  6300  unixpid  6302  xpcoid  6308  fodomr  9164  xpfiOLD  9355  fodomfir  9364  iundom2g  10576  hashxplem  14468  dmtrclfv  15053  ramcl  17063  0subcat  17879  mat0dimbas0  22462  mavmul0g  22549  txindislem  23631  txhaus  23645  tmdgsum  24093  ust0  24218  ehl0  25441  mbf0  25659  hashxpe  32799  gsumpart  33045  erlval  33250  fracbas  33294  sibf0  34314  lpadlem3  34671  mexval2  35486  poimirlem5  37610  poimirlem10  37615  poimirlem22  37627  poimirlem23  37628  poimirlem26  37631  poimirlem28  37633  0no  43426  0heALT  43774  0funcg2  48893  0funcALT  48897