Theorem xp0 5745

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 4290	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 782	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 199	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1819	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1819	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5667	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 199	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4306	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∅c0 4285  ⟨cop 4587   × cxp 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3907  df-nul 4286  df-opab 5162  df-xp 5651

This theorem is referenced by:  xpnz  6141  xpdisj2  6144  difxp1  6147  dmxpss  6153  rnxpid  6155  xpcan  6158  unixp  6265  dfpo2  6279  fconst5  7186  dfac5lem3  10078  djuassen  10132  xpdjuen  10133  alephadd  10532  fpwwe2lem12  10597  0ssc  17853  fuchom  17980  frmdplusg  18871  mulgfval  19094  mulgfvalALT  19095  mulgfvi  19098  ga0  19321  efgval  19740  psrplusg  21969  psrvscafval  21980  opsrle  22080  ply1plusgfvi  22283  txindislem  23673  txhaus  23687  0met  24406  2ndimaxp  32798  aciunf1  32815  hashxpe  32959  mbfmcst  34517  0rrv  34709  sate0  35729  mexval  35816  mdvval  35818  mpstval  35849  elima4  36090  finxp00  37860  isbnd3  38247  zrdivrng  38416  dmrnxp  49422  mofeu  49433  fucofvalne  49910