Theorem xp0 5751

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4279  ⟨cop 4590   × cxp 5649

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-nul 4280  df-opab 5168  df-xp 5657

This theorem is used by:  xpnz  6149  xpdisj2  6152  difxp1  6155  dmxpss  6162  rnxpid  6164  xpcan  6167  unixp  6278  dfpo2  6292  fconst5  7204  dfac5lem3  10185  djuassen  10238  xpdjuen  10239  alephadd  10643  fpwwe2lem12  10708  0ssc  17992  fuchom  18119  frmdplusg  19030  mulgfval  19259  mulgfvalALT  19260  mulgfvi  19263  ga0  19492  efgval  19911  psrplusg  22225  psrvscafval  22236  opsrle  22336  ply1plusgfvi  22539  txindislem  23932  txhaus  23946  0met  24665  2ndimaxp  33222  aciunf1  33239  hashxpe  33381  mbfmcst  34874  0rrv  35066  sate0  36149  mexval  36236  mdvval  36238  mpstval  36269  elima4  36510  finxp00  38293  isbnd3  38686  zrdivrng  38855  dmrnxp  49891  mofeu  49902  fucofvalne  50377