![]() |
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 4343 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | simprl 771 | . . . . . 6 ⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅) | |
3 | 1, 2 | mto 197 | . . . . 5 ⊢ ¬ (𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
4 | 3 | nex 1796 | . . . 4 ⊢ ¬ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
5 | 4 | nex 1796 | . . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
6 | elxp 5711 | . . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))) | |
7 | 5, 6 | mtbir 323 | . 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴) |
8 | 7 | nel0 4359 | 1 ⊢ (∅ × 𝐴) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1536 ∃wex 1775 ∈ wcel 2105 ∅c0 4338 〈cop 4636 × cxp 5686 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-opab 5210 df-xp 5694 |
This theorem is referenced by: dmxpid 5943 csbres 6002 res0 6003 xp0 6179 xpnz 6180 xpdisj1 6182 difxp2 6187 xpcan2 6198 xpima 6203 unixp 6303 unixpid 6305 xpcoid 6311 fodomr 9166 xpfiOLD 9356 fodomfir 9365 iundom2g 10577 hashxplem 14468 dmtrclfv 15053 ramcl 17062 0subcat 17888 mat0dimbas0 22487 mavmul0g 22574 txindislem 23656 txhaus 23670 tmdgsum 24118 ust0 24243 ehl0 25464 mbf0 25682 hashxpe 32816 gsumpart 33042 erlval 33244 fracbas 33286 sibf0 34315 lpadlem3 34671 mexval2 35487 poimirlem5 37611 poimirlem10 37616 poimirlem22 37628 poimirlem23 37629 poimirlem26 37632 poimirlem28 37634 0no 43424 0heALT 43772 |
Copyright terms: Public domain | W3C validator |