MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0xp Structured version   Visualization version   GIF version

Theorem 0xp 5108
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.
StepHypRef Expression
1 elxp 5041 . . 3 (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)))
2 noel 3873 . . . . . . 7 ¬ 𝑥 ∈ ∅
3 simprl 789 . . . . . . 7 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)) → 𝑥 ∈ ∅)
42, 3mto 186 . . . . . 6 ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
54nex 1720 . . . . 5 ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
65nex 1720 . . . 4 ¬ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
7 noel 3873 . . . 4 ¬ 𝑧 ∈ ∅
86, 72false 363 . . 3 (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)) ↔ 𝑧 ∈ ∅)
91, 8bitri 262 . 2 (𝑧 ∈ (∅ × 𝐴) ↔ 𝑧 ∈ ∅)
109eqriv 2602 1 (∅ × 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wex 1694  wcel 1975  c0 3869  cop 4126   × cxp 5022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-opab 4634  df-xp 5030
This theorem is referenced by:  dmxpid  5249  csbres  5303  res0  5304  xp0  5453  xpnz  5454  xpdisj1  5456  difxp2  5461  xpcan2  5472  xpima  5477  unixp  5567  unixpid  5569  xpcoid  5575  fodomr  7969  xpfi  8089  cdaassen  8860  iundom2g  9214  alephadd  9251  hashxplem  13028  dmtrclfv  13549  ramcl  15513  0subcat  16263  mat0dimbas0  20029  mavmul0g  20116  txindislem  21184  txhaus  21198  tmdgsum  21647  ust0  21771  sibf0  29525  mexval2  30456  poimirlem5  32383  poimirlem10  32388  poimirlem22  32400  poimirlem23  32401  poimirlem26  32404  poimirlem28  32406  0mbf  32424  0heALT  36896
  Copyright terms: Public domain W3C validator