Theorem xp0 6015

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 5649	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5745	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6014	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 5999	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2852	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1537  ∅c0 4291   × cxp 5553  ^◡ccnv 5554

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562  df-cnv 5563

This theorem is referenced by:  xpnz  6016  xpdisj2  6019  difxp1  6022  dmxpss  6028  rnxpid  6030  xpcan  6033  unixp  6133  fconst5  6968  dfac5lem3  9551  djuassen  9604  xpdjuen  9605  alephadd  9999  fpwwe2lem13  10064  0ssc  17107  fuchom  17231  frmdplusg  18019  mulgfval  18226  mulgfvalALT  18227  mulgfvi  18230  ga0  18428  efgval  18843  psrplusg  20161  psrvscafval  20170  opsrle  20256  ply1plusgfvi  20410  txindislem  22241  txhaus  22255  0met  22976  aciunf1  30408  hashxpe  30529  mbfmcst  31517  0rrv  31709  sate0  32662  mexval  32749  mdvval  32751  mpstval  32782  dfpo2  32991  elima4  33019  finxp00  34686  isbnd3  35077  zrdivrng  35246