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

Theorem xp0 5991
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.)
Assertion
Ref Expression
xp0 (𝐴 × ∅) = ∅

Proof of Theorem xp0
StepHypRef Expression
1 0xp 5625 . . 3 (∅ × 𝐴) = ∅
21cnveqi 5721 . 2 (∅ × 𝐴) =
3 cnvxp 5990 . 2 (∅ × 𝐴) = (𝐴 × ∅)
4 cnv0 5975 . 2 ∅ = ∅
52, 3, 43eqtr3i 2851 1 (𝐴 × ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  c0 4269   × cxp 5529  ccnv 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-br 5043  df-opab 5105  df-xp 5537  df-rel 5538  df-cnv 5539
This theorem is referenced by:  xpnz  5992  xpdisj2  5995  difxp1  5998  dmxpss  6004  rnxpid  6006  xpcan  6009  unixp  6109  fconst5  6944  dfac5lem3  9529  djuassen  9582  xpdjuen  9583  alephadd  9977  fpwwe2lem13  10042  0ssc  17086  fuchom  17210  frmdplusg  17998  mulgfval  18205  mulgfvalALT  18206  mulgfvi  18209  ga0  18407  efgval  18822  psrplusg  20137  psrvscafval  20146  opsrle  20232  ply1plusgfvi  20386  txindislem  22217  txhaus  22231  0met  22952  aciunf1  30395  hashxpe  30516  mbfmcst  31525  0rrv  31717  sate0  32670  mexval  32757  mdvval  32759  mpstval  32790  dfpo2  32999  elima4  33027  finxp00  34700  isbnd3  35098  zrdivrng  35267
  Copyright terms: Public domain W3C validator