Theorem xp0 5766

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∅c0 4289  ⟨cop 4600   × cxp 5664

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-dif 3911  df-nul 4290  df-opab 5179  df-xp 5672

This theorem is used by:  xpnz  6161  xpdisj2  6164  difxp1  6167  dmxpss  6174  rnxpid  6176  xpcan  6179  unixp  6290  dfpo2  6304  fconst5  7211  dfac5lem3  10128  djuassen  10181  xpdjuen  10182  alephadd  10580  fpwwe2lem12  10645  0ssc  17919  fuchom  18046  frmdplusg  18944  mulgfval  19166  mulgfvalALT  19167  mulgfvi  19170  ga0  19399  efgval  19818  psrplusg  22124  psrvscafval  22135  opsrle  22235  ply1plusgfvi  22438  txindislem  23827  txhaus  23841  0met  24560  2ndimaxp  33028  aciunf1  33045  hashxpe  33189  mbfmcst  34681  0rrv  34873  sate0  35928  mexval  36015  mdvval  36017  mpstval  36048  elima4  36289  finxp00  38089  isbnd3  38476  zrdivrng  38645  dmrnxp  49656  mofeu  49667  fucofvalne  50144