Theorem 0xp 5793

Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
0xp	⊢ (∅ × 𝐴) = ∅

Proof of Theorem 0xp

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4360	. . . . . 6 ⊢ ¬ 𝑥 ∈ ∅
2		simprl 770	. . . . . 6 ⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅)
3	1, 2	mto 197	. . . . 5 ⊢ ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
4	3	nex 1798	. . . 4 ⊢ ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
5	4	nex 1798	. . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))
6		elxp 5718	. . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)))
7	5, 6	mtbir 323	. 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴)
8	7	nel0 4377	1 ⊢ (∅ × 𝐴) = ∅

Syntax hints:   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∅c0 4352  ⟨cop 4654   × cxp 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-xp 5701

This theorem is referenced by:  dmxpid  5950  csbres  6007  res0  6008  xp0  6184  xpnz  6185  xpdisj1  6187  difxp2  6192  xpcan2  6203  xpima  6208  unixp  6308  unixpid  6310  xpcoid  6316  fodomr  9188  xpfiOLD  9381  fodomfir  9390  iundom2g  10603  hashxplem  14476  dmtrclfv  15061  ramcl  17070  0subcat  17896  mat0dimbas0  22485  mavmul0g  22572  txindislem  23654  txhaus  23668  tmdgsum  24116  ust0  24241  ehl0  25462  mbf0  25680  hashxpe  32806  gsumpart  33030  erlval  33222  fracbas  33264  sibf0  34291  lpadlem3  34647  mexval2  35463  poimirlem5  37577  poimirlem10  37582  poimirlem22  37594  poimirlem23  37595  poimirlem26  37598  poimirlem28  37600  0no  43392  0heALT  43740