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

Theorem 0xp 5782
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 4337 . . . . . 6 ¬ 𝑥 ∈ ∅
2 simprl 771 . . . . . 6 ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)) → 𝑥 ∈ ∅)
31, 2mto 197 . . . . 5 ¬ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
43nex 1800 . . . 4 ¬ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
54nex 1800 . . 3 ¬ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴))
6 elxp 5706 . . 3 (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ ∅ ∧ 𝑦𝐴)))
75, 6mtbir 323 . 2 ¬ 𝑧 ∈ (∅ × 𝐴)
87nel0 4353 1 (∅ × 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wex 1779  wcel 2108  c0 4332  cop 4630   × cxp 5681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-opab 5204  df-xp 5689
This theorem is referenced by:  dmxpid  5939  csbres  5998  res0  5999  xp0  6176  xpnz  6177  xpdisj1  6179  difxp2  6184  xpcan2  6195  xpima  6200  unixp  6300  unixpid  6302  xpcoid  6308  fodomr  9164  xpfiOLD  9355  fodomfir  9364  iundom2g  10576  hashxplem  14468  dmtrclfv  15053  ramcl  17063  0subcat  17879  mat0dimbas0  22462  mavmul0g  22549  txindislem  23631  txhaus  23645  tmdgsum  24093  ust0  24218  ehl0  25441  mbf0  25659  hashxpe  32799  gsumpart  33045  erlval  33250  fracbas  33294  sibf0  34314  lpadlem3  34671  mexval2  35486  poimirlem5  37610  poimirlem10  37615  poimirlem22  37627  poimirlem23  37628  poimirlem26  37631  poimirlem28  37633  0no  43426  0heALT  43774  0funcg2  48893  0funcALT  48897
  Copyright terms: Public domain W3C validator