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

Theorem xp0 6035
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 5660 . . 3 (∅ × 𝐴) = ∅
21cnveqi 5757 . 2 (∅ × 𝐴) =
3 cnvxp 6034 . 2 (∅ × 𝐴) = (𝐴 × ∅)
4 cnv0 6018 . 2 ∅ = ∅
52, 3, 43eqtr3i 2774 1 (𝐴 × ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  c0 4251   × cxp 5563  ccnv 5564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3071  df-v 3422  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-op 4562  df-br 5068  df-opab 5130  df-xp 5571  df-rel 5572  df-cnv 5573
This theorem is referenced by:  xpnz  6036  xpdisj2  6039  difxp1  6042  dmxpss  6048  rnxpid  6050  xpcan  6053  unixp  6159  dfpo2  6173  fconst5  7039  dfac5lem3  9763  djuassen  9816  xpdjuen  9817  alephadd  10215  fpwwe2lem12  10280  0ssc  17367  fuchom  17493  fuchomOLD  17494  frmdplusg  18305  mulgfval  18514  mulgfvalALT  18515  mulgfvi  18518  ga0  18716  efgval  19131  psrplusg  20930  psrvscafval  20939  opsrle  21028  ply1plusgfvi  21187  txindislem  22554  txhaus  22568  0met  23288  2ndimaxp  30727  aciunf1  30744  hashxpe  30871  mbfmcst  31962  0rrv  32154  sate0  33113  mexval  33200  mdvval  33202  mpstval  33233  elima4  33492  finxp00  35336  isbnd3  35705  zrdivrng  35874  mofeu  45876
  Copyright terms: Public domain W3C validator