Theorem xp0 5731

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 4278	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 773	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1802	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1802	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5653	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 197	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4294	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4273  ⟨cop 4573   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-nul 4274  df-opab 5148  df-xp 5637

This theorem is referenced by:  xpnz  6123  xpdisj2  6126  difxp1  6129  dmxpss  6135  rnxpid  6137  xpcan  6140  unixp  6246  dfpo2  6260  fconst5  7161  dfac5lem3  10047  djuassen  10101  xpdjuen  10102  alephadd  10500  fpwwe2lem12  10565  0ssc  17804  fuchom  17931  frmdplusg  18822  mulgfval  19045  mulgfvalALT  19046  mulgfvi  19049  ga0  19273  efgval  19692  psrplusg  21916  psrvscafval  21927  opsrle  22025  ply1plusgfvi  22205  txindislem  23598  txhaus  23612  0met  24331  2ndimaxp  32719  aciunf1  32736  hashxpe  32880  mbfmcst  34403  0rrv  34595  sate0  35597  mexval  35684  mdvval  35686  mpstval  35717  elima4  35958  finxp00  37718  isbnd3  38105  zrdivrng  38274  dmrnxp  49312  mofeu  49323  fucofvalne  49800