Theorem xp0 5732

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4287  ⟨cop 4588   × cxp 5630

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-nul 4288  df-opab 5163  df-xp 5638

This theorem is referenced by:  xpnz  6125  xpdisj2  6128  difxp1  6131  dmxpss  6137  rnxpid  6139  xpcan  6142  unixp  6248  dfpo2  6262  fconst5  7162  dfac5lem3  10047  djuassen  10101  xpdjuen  10102  alephadd  10500  fpwwe2lem12  10565  0ssc  17773  fuchom  17900  frmdplusg  18791  mulgfval  19011  mulgfvalALT  19012  mulgfvi  19015  ga0  19239  efgval  19658  psrplusg  21904  psrvscafval  21916  opsrle  22014  ply1plusgfvi  22194  txindislem  23589  txhaus  23603  0met  24322  2ndimaxp  32735  aciunf1  32752  hashxpe  32897  mbfmcst  34436  0rrv  34628  sate0  35628  mexval  35715  mdvval  35717  mpstval  35748  elima4  35989  finxp00  37651  isbnd3  38029  zrdivrng  38198  dmrnxp  49190  mofeu  49201  fucofvalne  49678