Theorem xp0 6111

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 5722	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5821	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6110	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6093	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2760	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4286   × cxp 5621  ^◡ccnv 5622

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 5238  ax-nul 5248  ax-pr 5374

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631

This theorem is referenced by:  xpnz  6112  xpdisj2  6115  difxp1  6118  dmxpss  6124  rnxpid  6126  xpcan  6129  unixp  6234  dfpo2  6248  fconst5  7146  dfac5lem3  10038  djuassen  10092  xpdjuen  10093  alephadd  10490  fpwwe2lem12  10555  0ssc  17762  fuchom  17889  frmdplusg  18746  mulgfval  18966  mulgfvalALT  18967  mulgfvi  18970  ga0  19195  efgval  19614  psrplusg  21861  psrvscafval  21873  opsrle  21970  ply1plusgfvi  22142  txindislem  23536  txhaus  23550  0met  24270  2ndimaxp  32603  aciunf1  32620  hashxpe  32765  mbfmcst  34226  0rrv  34418  sate0  35387  mexval  35474  mdvval  35476  mpstval  35507  elima4  35748  finxp00  37375  isbnd3  37763  zrdivrng  37932  dmrnxp  48822  mofeu  48833  fucofvalne  49311