Theorem xp0 5725

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 4273	. . . . . 6 ⊢ ¬ 𝑦 ∈ ∅
2		simprr 778	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)) → 𝑦 ∈ ∅)
3	1, 2	mto 198	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
4	3	nex 1807	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
5	4	nex 1807	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅))
6		elxpi 5647	. . 3 ⊢ (𝑧 ∈ (𝐴 × ∅) → ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅)))
7	5, 6	mto 198	. 2 ⊢ ¬ 𝑧 ∈ (𝐴 × ∅)
8	7	nel0 4289	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4268  ⟨cop 4568   × cxp 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-dif 3893  df-nul 4269  df-opab 5142  df-xp 5631

This theorem is referenced by:  xpnz  6117  xpdisj2  6120  difxp1  6123  dmxpss  6129  rnxpid  6131  xpcan  6134  unixp  6240  dfpo2  6254  fconst5  7157  dfac5lem3  10045  djuassen  10099  xpdjuen  10100  alephadd  10498  fpwwe2lem12  10563  0ssc  17802  fuchom  17929  frmdplusg  18820  mulgfval  19043  mulgfvalALT  19044  mulgfvi  19047  ga0  19271  efgval  19690  psrplusg  21919  psrvscafval  21930  opsrle  22030  ply1plusgfvi  22233  txindislem  23623  txhaus  23637  0met  24356  2ndimaxp  32745  aciunf1  32762  hashxpe  32906  mbfmcst  34450  0rrv  34642  sate0  35650  mexval  35737  mdvval  35739  mpstval  35770  elima4  36011  finxp00  37771  isbnd3  38158  zrdivrng  38327  dmrnxp  49334  mofeu  49345  fucofvalne  49822