Theorem xp0 5763

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

Syntax hints:   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4287  ⟨cop 4596   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-nul 4288  df-opab 5175  df-xp 5669

This theorem is referenced by:  xpnz  6158  xpdisj2  6161  difxp1  6164  dmxpss  6171  rnxpid  6173  xpcan  6176  unixp  6285  dfpo2  6299  fconst5  7206  dfac5lem3  10110  djuassen  10163  xpdjuen  10164  alephadd  10563  fpwwe2lem12  10628  0ssc  17895  fuchom  18022  frmdplusg  18914  mulgfval  19136  mulgfvalALT  19137  mulgfvi  19140  ga0  19369  efgval  19788  psrplusg  22068  psrvscafval  22079  opsrle  22179  ply1plusgfvi  22382  txindislem  23771  txhaus  23785  0met  24504  2ndimaxp  32969  aciunf1  32986  hashxpe  33130  mbfmcst  34627  0rrv  34819  sate0  35885  mexval  35972  mdvval  35974  mpstval  36005  elima4  36246  finxp00  38026  isbnd3  38413  zrdivrng  38582  dmrnxp  49592  mofeu  49603  fucofvalne  50080