Theorem xp0 6131

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 5737	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5838	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6130	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6113	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2760	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4296   × cxp 5636  ^◡ccnv 5637

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 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-cnv 5646

This theorem is referenced by:  xpnz  6132  xpdisj2  6135  difxp1  6138  dmxpss  6144  rnxpid  6146  xpcan  6149  unixp  6255  dfpo2  6269  fconst5  7180  dfac5lem3  10078  djuassen  10132  xpdjuen  10133  alephadd  10530  fpwwe2lem12  10595  0ssc  17799  fuchom  17926  frmdplusg  18781  mulgfval  19001  mulgfvalALT  19002  mulgfvi  19005  ga0  19230  efgval  19647  psrplusg  21845  psrvscafval  21857  opsrle  21954  ply1plusgfvi  22126  txindislem  23520  txhaus  23534  0met  24254  2ndimaxp  32570  aciunf1  32587  hashxpe  32732  mbfmcst  34250  0rrv  34442  sate0  35402  mexval  35489  mdvval  35491  mpstval  35522  elima4  35763  finxp00  37390  isbnd3  37778  zrdivrng  37947  dmrnxp  48825  mofeu  48836  fucofvalne  49314