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 5199 | . . 3 ⊢ (∅ × 𝐴) = ∅ | |
2 | 1 | cnveqi 5297 | . 2 ⊢ ◡(∅ × 𝐴) = ◡∅ |
3 | cnvxp 5551 | . 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅) | |
4 | cnv0 5535 | . 2 ⊢ ◡∅ = ∅ | |
5 | 2, 3, 4 | 3eqtr3i 2652 | 1 ⊢ (𝐴 × ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 ∅c0 3915 × cxp 5112 ◡ccnv 5113 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-xp 5120 df-rel 5121 df-cnv 5122 |
This theorem is referenced by: xpnz 5553 xpdisj2 5556 difxp1 5559 dmxpss 5565 rnxpid 5567 xpcan 5570 unixp 5668 fconst5 6471 dfac5lem3 8948 xpcdaen 9005 fpwwe2lem13 9464 comfffval 16358 0ssc 16497 fuchom 16621 xpccofval 16822 frmdplusg 17391 mulgfval 17542 mulgfvi 17545 ga0 17731 symgplusg 17809 efgval 18130 psrplusg 19381 psrvscafval 19390 opsrle 19475 ply1plusgfvi 19612 txindislem 21436 txhaus 21450 0met 22171 aciunf1 29463 mbfmcst 30321 0rrv 30513 mexval 31399 mdvval 31401 mpstval 31432 dfpo2 31645 elima4 31679 finxp00 33239 isbnd3 33583 zrdivrng 33752 |
Copyright terms: Public domain | W3C validator |