Theorem xp0 5752

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

Syntax hints:   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∅c0 4288  ⟨cop 4591   × cxp 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3910  df-nul 4289  df-opab 5168  df-xp 5658

This theorem is referenced by:  xpnz  6148  xpdisj2  6151  difxp1  6154  dmxpss  6161  rnxpid  6163  xpcan  6166  unixp  6273  dfpo2  6287  fconst5  7194  dfac5lem3  10097  djuassen  10150  xpdjuen  10151  alephadd  10550  fpwwe2lem12  10615  0ssc  17884  fuchom  18011  frmdplusg  18903  mulgfval  19126  mulgfvalALT  19127  mulgfvi  19130  ga0  19359  efgval  19778  psrplusg  22047  psrvscafval  22058  opsrle  22158  ply1plusgfvi  22361  txindislem  23751  txhaus  23765  0met  24484  2ndimaxp  32903  aciunf1  32920  hashxpe  33064  mbfmcst  34566  0rrv  34758  sate0  35778  mexval  35865  mdvval  35867  mpstval  35898  elima4  36139  finxp00  37908  isbnd3  38295  zrdivrng  38464  dmrnxp  49466  mofeu  49477  fucofvalne  49954