Theorem xp0 6134

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 5740	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5841	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6133	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6116	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2761	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4299   × cxp 5639  ^◡ccnv 5640

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649

This theorem is referenced by:  xpnz  6135  xpdisj2  6138  difxp1  6141  dmxpss  6147  rnxpid  6149  xpcan  6152  unixp  6258  dfpo2  6272  fconst5  7183  dfac5lem3  10085  djuassen  10139  xpdjuen  10140  alephadd  10537  fpwwe2lem12  10602  0ssc  17806  fuchom  17933  frmdplusg  18788  mulgfval  19008  mulgfvalALT  19009  mulgfvi  19012  ga0  19237  efgval  19654  psrplusg  21852  psrvscafval  21864  opsrle  21961  ply1plusgfvi  22133  txindislem  23527  txhaus  23541  0met  24261  2ndimaxp  32577  aciunf1  32594  hashxpe  32739  mbfmcst  34257  0rrv  34449  sate0  35409  mexval  35496  mdvval  35498  mpstval  35529  elima4  35770  finxp00  37397  isbnd3  37785  zrdivrng  37954  dmrnxp  48829  mofeu  48840  fucofvalne  49318