Theorem xp0 5722

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

Syntax hints:   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4274  ⟨cop 4574   × cxp 5620

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 3893  df-nul 4275  df-opab 5149  df-xp 5628

This theorem is referenced by:  xpnz  6115  xpdisj2  6118  difxp1  6121  dmxpss  6127  rnxpid  6129  xpcan  6132  unixp  6238  dfpo2  6252  fconst5  7152  dfac5lem3  10036  djuassen  10090  xpdjuen  10091  alephadd  10489  fpwwe2lem12  10554  0ssc  17762  fuchom  17889  frmdplusg  18780  mulgfval  19003  mulgfvalALT  19004  mulgfvi  19007  ga0  19231  efgval  19650  psrplusg  21893  psrvscafval  21905  opsrle  22003  ply1plusgfvi  22183  txindislem  23576  txhaus  23590  0met  24309  2ndimaxp  32708  aciunf1  32725  hashxpe  32870  mbfmcst  34409  0rrv  34601  sate0  35603  mexval  35690  mdvval  35692  mpstval  35723  elima4  35964  finxp00  37714  isbnd3  38096  zrdivrng  38265  dmrnxp  49270  mofeu  49281  fucofvalne  49758