Theorem xp0 6147

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

Step	Hyp	Ref	Expression
1		0xp 5753	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5854	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6146	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6129	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2766	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4308   × cxp 5652  ^◡ccnv 5653

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-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662

This theorem is referenced by:  xpnz  6148  xpdisj2  6151  difxp1  6154  dmxpss  6160  rnxpid  6162  xpcan  6165  unixp  6271  dfpo2  6285  fconst5  7198  dfac5lem3  10139  djuassen  10193  xpdjuen  10194  alephadd  10591  fpwwe2lem12  10656  0ssc  17850  fuchom  17977  frmdplusg  18832  mulgfval  19052  mulgfvalALT  19053  mulgfvi  19056  ga0  19281  efgval  19698  psrplusg  21896  psrvscafval  21908  opsrle  22005  ply1plusgfvi  22177  txindislem  23571  txhaus  23585  0met  24305  2ndimaxp  32624  aciunf1  32641  hashxpe  32786  mbfmcst  34291  0rrv  34483  sate0  35437  mexval  35524  mdvval  35526  mpstval  35557  elima4  35793  finxp00  37420  isbnd3  37808  zrdivrng  37977  dmrnxp  48815  mofeu  48826  fucofvalne  49236