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

Theorem 0xp 5619
 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 noel 4231 . . . . . 6 ¬ 𝑥 ∈ ∅
2 simprl 771 . . . . . 6 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)) → 𝑥 ∈ ∅)
31, 2mto 200 . . . . 5 ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
43nex 1803 . . . 4 ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
54nex 1803 . . 3 ¬ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
6 elxp 5548 . . 3 (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)))
75, 6mtbir 327 . 2 ¬ 𝑧 ∈ (∅ × 𝐴)
87nel0 4250 1 (∅ × 𝐴) = ∅
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∅c0 4226  ⟨cop 4529   × cxp 5523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-dif 3862  df-un 3864  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-opab 5096  df-xp 5531 This theorem is referenced by:  dmxpid  5772  csbres  5827  res0  5828  xp0  5988  xpnz  5989  xpdisj1  5991  difxp2  5996  xpcan2  6007  xpima  6012  unixp  6112  unixpid  6114  xpcoid  6120  fodomr  8691  xpfi  8823  iundom2g  10001  hashxplem  13845  dmtrclfv  14426  ramcl  16421  0subcat  17168  mat0dimbas0  21167  mavmul0g  21254  txindislem  22334  txhaus  22348  tmdgsum  22796  ust0  22921  ehl0  24118  mbf0  24335  hashxpe  30652  gsumpart  30842  sibf0  31821  lpadlem3  32178  mexval2  32982  poimirlem5  35343  poimirlem10  35348  poimirlem22  35360  poimirlem23  35361  poimirlem26  35364  poimirlem28  35366  0heALT  40858
 Copyright terms: Public domain W3C validator