Theorem xp0 6049

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 5674	. . 3 ⊢ (∅ × 𝐴) = ∅
2	1	cnveqi 5771	. 2 ⊢ ◡(∅ × 𝐴) = ◡∅
3		cnvxp 6048	. 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅)
4		cnv0 6032	. 2 ⊢ ◡∅ = ∅
5	2, 3, 4	3eqtr3i 2775	1 ⊢ (𝐴 × ∅) = ∅

Syntax hints:   = wceq 1543  ∅c0 4254   × cxp 5577  ^◡ccnv 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5585  df-rel 5586  df-cnv 5587

This theorem is referenced by:  xpnz  6050  xpdisj2  6053  difxp1  6056  dmxpss  6062  rnxpid  6064  xpcan  6067  unixp  6173  dfpo2  6187  fconst5  7060  dfac5lem3  9787  djuassen  9840  xpdjuen  9841  alephadd  10239  fpwwe2lem12  10304  0ssc  17443  fuchom  17569  fuchomOLD  17570  frmdplusg  18383  mulgfval  18592  mulgfvalALT  18593  mulgfvi  18596  ga0  18794  efgval  19213  psrplusg  21035  psrvscafval  21044  opsrle  21133  ply1plusgfvi  21298  txindislem  22667  txhaus  22681  0met  23402  2ndimaxp  30860  aciunf1  30877  hashxpe  31004  mbfmcst  32101  0rrv  32293  sate0  33252  mexval  33339  mdvval  33341  mpstval  33372  elima4  33631  finxp00  35479  isbnd3  35848  zrdivrng  36017  mofeu  46036