![]() |
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 5773 | . . 3 ⊢ (∅ × 𝐴) = ∅ | |
2 | 1 | cnveqi 5873 | . 2 ⊢ ◡(∅ × 𝐴) = ◡∅ |
3 | cnvxp 6154 | . 2 ⊢ ◡(∅ × 𝐴) = (𝐴 × ∅) | |
4 | cnv0 6138 | . 2 ⊢ ◡∅ = ∅ | |
5 | 2, 3, 4 | 3eqtr3i 2769 | 1 ⊢ (𝐴 × ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∅c0 4322 × cxp 5674 ◡ccnv 5675 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-rel 5683 df-cnv 5684 |
This theorem is referenced by: xpnz 6156 xpdisj2 6159 difxp1 6162 dmxpss 6168 rnxpid 6170 xpcan 6173 unixp 6279 dfpo2 6293 fconst5 7204 dfac5lem3 10117 djuassen 10170 xpdjuen 10171 alephadd 10569 fpwwe2lem12 10634 0ssc 17784 fuchom 17910 fuchomOLD 17911 frmdplusg 18732 mulgfval 18947 mulgfvalALT 18948 mulgfvi 18951 ga0 19157 efgval 19580 psrplusg 21492 psrvscafval 21501 opsrle 21594 ply1plusgfvi 21756 txindislem 23129 txhaus 23143 0met 23864 2ndimaxp 31860 aciunf1 31876 hashxpe 32007 mbfmcst 33247 0rrv 33439 sate0 34395 mexval 34482 mdvval 34484 mpstval 34515 elima4 34736 finxp00 36272 isbnd3 36641 zrdivrng 36810 mofeu 47468 |
Copyright terms: Public domain | W3C validator |