Theorem xp0 5724

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 772	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1801	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1801	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5646	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 197	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4306	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4285  ⟨cop 4586   × cxp 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-nul 4286  df-opab 5161  df-xp 5630

This theorem is referenced by:  xpnz  6117  xpdisj2  6120  difxp1  6123  dmxpss  6129  rnxpid  6131  xpcan  6134  unixp  6240  dfpo2  6254  fconst5  7152  dfac5lem3  10035  djuassen  10089  xpdjuen  10090  alephadd  10488  fpwwe2lem12  10553  0ssc  17761  fuchom  17888  frmdplusg  18779  mulgfval  18999  mulgfvalALT  19000  mulgfvi  19003  ga0  19227  efgval  19646  psrplusg  21892  psrvscafval  21904  opsrle  22002  ply1plusgfvi  22182  txindislem  23577  txhaus  23591  0met  24310  2ndimaxp  32724  aciunf1  32741  hashxpe  32887  mbfmcst  34416  0rrv  34608  sate0  35609  mexval  35696  mdvval  35698  mpstval  35729  elima4  35970  finxp00  37603  isbnd3  37981  zrdivrng  38150  dmrnxp  49078  mofeu  49089  fucofvalne  49566