Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0xp | 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, 4-Jul-1994.) |
Ref | Expression |
---|---|
0xp | ⊢ (∅ × 𝐴) = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 4295 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | simprl 769 | . . . . . 6 ⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅) | |
3 | 1, 2 | mto 199 | . . . . 5 ⊢ ¬ (𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
4 | 3 | nex 1797 | . . . 4 ⊢ ¬ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
5 | 4 | nex 1797 | . . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
6 | elxp 5572 | . . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))) | |
7 | 5, 6 | mtbir 325 | . 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴) |
8 | 7 | nel0 4310 | 1 ⊢ (∅ × 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∅c0 4290 〈cop 4566 × cxp 5547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-opab 5121 df-xp 5555 |
This theorem is referenced by: dmxpid 5794 csbres 5850 res0 5851 xp0 6009 xpnz 6010 xpdisj1 6012 difxp2 6017 xpcan2 6028 xpima 6033 unixp 6127 unixpid 6129 xpcoid 6135 fodomr 8662 xpfi 8783 iundom2g 9956 hashxplem 13788 dmtrclfv 14372 ramcl 16359 0subcat 17102 mat0dimbas0 21069 mavmul0g 21156 txindislem 22235 txhaus 22249 tmdgsum 22697 ust0 22822 ehl0 24014 mbf0 24229 hashxpe 30523 sibf0 31587 lpadlem3 31944 mexval2 32745 poimirlem5 34891 poimirlem10 34896 poimirlem22 34908 poimirlem23 34909 poimirlem26 34912 poimirlem28 34914 0heALT 40122 |
Copyright terms: Public domain | W3C validator |