Theorem xp0 5724

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 5646	. . 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 5622

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 5630

This theorem is referenced by:  xpnz  6117  xpdisj2  6120  difxp1  6123  dmxpss  6129  rnxpid  6131  xpcan  6134  unixp  6240  dfpo2  6254  fconst5  7154  dfac5lem3  10038  djuassen  10092  xpdjuen  10093  alephadd  10491  fpwwe2lem12  10556  0ssc  17795  fuchom  17922  frmdplusg  18813  mulgfval  19036  mulgfvalALT  19037  mulgfvi  19040  ga0  19264  efgval  19683  psrplusg  21926  psrvscafval  21937  opsrle  22035  ply1plusgfvi  22215  txindislem  23608  txhaus  23622  0met  24341  2ndimaxp  32734  aciunf1  32751  hashxpe  32895  mbfmcst  34419  0rrv  34611  sate0  35613  mexval  35700  mdvval  35702  mpstval  35733  elima4  35974  finxp00  37732  isbnd3  38119  zrdivrng  38288  dmrnxp  49324  mofeu  49335  fucofvalne  49812