Theorem xp0 6105

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 5715	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5814	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6104	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6087	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2762	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1541  ∅c0 4283   × cxp 5614  ^◡ccnv 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-xp 5622  df-rel 5623  df-cnv 5624

This theorem is referenced by:  xpnz  6106  xpdisj2  6109  difxp1  6112  dmxpss  6118  rnxpid  6120  xpcan  6123  unixp  6229  dfpo2  6243  fconst5  7140  dfac5lem3  10013  djuassen  10067  xpdjuen  10068  alephadd  10465  fpwwe2lem12  10530  0ssc  17741  fuchom  17868  frmdplusg  18759  mulgfval  18979  mulgfvalALT  18980  mulgfvi  18983  ga0  19208  efgval  19627  psrplusg  21871  psrvscafval  21883  opsrle  21980  ply1plusgfvi  22152  txindislem  23546  txhaus  23560  0met  24279  2ndimaxp  32623  aciunf1  32640  hashxpe  32784  mbfmcst  34267  0rrv  34459  sate0  35447  mexval  35534  mdvval  35536  mpstval  35567  elima4  35808  finxp00  37435  isbnd3  37823  zrdivrng  37992  dmrnxp  48867  mofeu  48878  fucofvalne  49356