Theorem xp0 5756

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) Avoid axioms. (Revised by TM, 1-Feb-2026.)

Assertion

Ref	Expression
xp0	⊢ (𝐴 × ∅) = ∅

Proof of Theorem xp0

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4286	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 785	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 200	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1833	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1833	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5677	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 200	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4305	1 ⊢ (𝐴 × ∅) = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∅c0 4281  ⟨cop 4838   × cxp 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-dif 4050  df-nul 4282  df-opab 5171  df-xp 5661

This theorem is used by:  xpnz  6162  xpdisj2  6165  difxp1  6168  dmxpss  6175  rnxpid  6177  xpcan  6180  unixp  6303  dfpo2  6317  fconst5  7235  dfac5lem3  10231  djuassen  10284  xpdjuen  10285  alephadd  10689  fpwwe2lem12  10754  0ssc  18041  fuchom  18168  frmdplusg  19079  mulgfval  19308  mulgfvalALT  19309  mulgfvi  19312  ga0  19542  efgval  19961  psrplusg  22275  psrvscafval  22286  opsrle  22386  ply1plusgfvi  22589  txindislem  23982  txhaus  23996  0met  24715  2ndimaxp  33312  aciunf1  33329  hashxpe  33469  mbfmcst  34961  0rrv  35153  sate0  36347  mexval  36434  mdvval  36436  mpstval  36467  elima4  36718  finxp00  38517  isbnd3  38910  zrdivrng  39079  dmrnxp  50153  mofeu  50164  fucofvalne  50652