Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xp0 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
xp0 | ⊢ (𝐴 × ∅) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0xp 5660 | . . 3 ⊢ (∅ × 𝐴) = ∅ | |
2 | 1 | cnveqi 5757 | . 2 ⊢ ◡(∅ × 𝐴) = ◡∅ |
3 | cnvxp 6034 | . 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅) | |
4 | cnv0 6018 | . 2 ⊢ ◡∅ = ∅ | |
5 | 2, 3, 4 | 3eqtr3i 2774 | 1 ⊢ (𝐴 × ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∅c0 4251 × cxp 5563 ◡ccnv 5564 |
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 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-sep 5206 ax-nul 5213 ax-pr 5336 |
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 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-rab 3071 df-v 3422 df-dif 3883 df-un 3885 df-in 3887 df-ss 3897 df-nul 4252 df-if 4454 df-sn 4556 df-pr 4558 df-op 4562 df-br 5068 df-opab 5130 df-xp 5571 df-rel 5572 df-cnv 5573 |
This theorem is referenced by: xpnz 6036 xpdisj2 6039 difxp1 6042 dmxpss 6048 rnxpid 6050 xpcan 6053 unixp 6159 dfpo2 6173 fconst5 7039 dfac5lem3 9763 djuassen 9816 xpdjuen 9817 alephadd 10215 fpwwe2lem12 10280 0ssc 17367 fuchom 17493 fuchomOLD 17494 frmdplusg 18305 mulgfval 18514 mulgfvalALT 18515 mulgfvi 18518 ga0 18716 efgval 19131 psrplusg 20930 psrvscafval 20939 opsrle 21028 ply1plusgfvi 21187 txindislem 22554 txhaus 22568 0met 23288 2ndimaxp 30727 aciunf1 30744 hashxpe 30871 mbfmcst 31962 0rrv 32154 sate0 33113 mexval 33200 mdvval 33202 mpstval 33233 elima4 33492 finxp00 35336 isbnd3 35705 zrdivrng 35874 mofeu 45876 |
Copyright terms: Public domain | W3C validator |