Theorem xp0 5750

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 4283	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 785	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 200	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1832	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1832	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5672	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 200	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4301	1 ⊢ (𝐴 × ∅) = ∅

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4278  ⟨cop 4834   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 4047  df-nul 4279  df-opab 5167  df-xp 5656

This theorem is used by:  xpnz  6149  xpdisj2  6152  difxp1  6155  dmxpss  6162  rnxpid  6164  xpcan  6167  unixp  6285  dfpo2  6299  fconst5  7212  dfac5lem3  10207  djuassen  10260  xpdjuen  10261  alephadd  10665  fpwwe2lem12  10730  0ssc  18017  fuchom  18144  frmdplusg  19055  mulgfval  19284  mulgfvalALT  19285  mulgfvi  19288  ga0  19517  efgval  19936  psrplusg  22250  psrvscafval  22261  opsrle  22361  ply1plusgfvi  22564  txindislem  23957  txhaus  23971  0met  24690  2ndimaxp  33287  aciunf1  33304  hashxpe  33445  mbfmcst  34937  0rrv  35129  sate0  36266  mexval  36353  mdvval  36355  mpstval  36386  elima4  36632  finxp00  38418  isbnd3  38811  zrdivrng  38980  dmrnxp  50041  mofeu  50052  fucofvalne  50540