Theorem xp0 5759

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 4287	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 785	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 200	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1833	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1833	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5681	. . 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 2145  ∅c0 4282  ⟨cop 4593   × cxp 5657

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-dif 3905  df-nul 4283  df-opab 5172  df-xp 5665

This theorem is used by:  xpnz  6155  xpdisj2  6158  difxp1  6161  dmxpss  6168  rnxpid  6170  xpcan  6173  unixp  6284  dfpo2  6298  fconst5  7209  dfac5lem3  10132  djuassen  10185  xpdjuen  10186  alephadd  10590  fpwwe2lem12  10655  0ssc  17932  fuchom  18059  frmdplusg  18969  mulgfval  19198  mulgfvalALT  19199  mulgfvi  19202  ga0  19431  efgval  19850  psrplusg  22158  psrvscafval  22169  opsrle  22269  ply1plusgfvi  22472  txindislem  23865  txhaus  23879  0met  24598  2ndimaxp  33127  aciunf1  33144  hashxpe  33286  mbfmcst  34778  0rrv  34970  sate0  36002  mexval  36089  mdvval  36091  mpstval  36122  elima4  36363  finxp00  38164  isbnd3  38542  zrdivrng  38711  dmrnxp  49773  mofeu  49784  fucofvalne  50259