| 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 4337 | . . . . . 6 ⊢ ¬ 𝑥 ∈ ∅ | |
| 2 | simprl 771 | . . . . . 6 ⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) → 𝑥 ∈ ∅) | |
| 3 | 1, 2 | mto 197 | . . . . 5 ⊢ ¬ (𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
| 4 | 3 | nex 1800 | . . . 4 ⊢ ¬ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
| 5 | 4 | nex 1800 | . . 3 ⊢ ¬ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴)) |
| 6 | elxp 5706 | . . 3 ⊢ (𝑧 ∈ (∅ × 𝐴) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ ∅ ∧ 𝑦 ∈ 𝐴))) | |
| 7 | 5, 6 | mtbir 323 | . 2 ⊢ ¬ 𝑧 ∈ (∅ × 𝐴) |
| 8 | 7 | nel0 4353 | 1 ⊢ (∅ × 𝐴) = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∅c0 4332 〈cop 4630 × cxp 5681 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2707 ax-sep 5294 ax-nul 5304 ax-pr 5430 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-opab 5204 df-xp 5689 |
| This theorem is referenced by: dmxpid 5939 csbres 5998 res0 5999 xp0 6176 xpnz 6177 xpdisj1 6179 difxp2 6184 xpcan2 6195 xpima 6200 unixp 6300 unixpid 6302 xpcoid 6308 fodomr 9164 xpfiOLD 9355 fodomfir 9364 iundom2g 10576 hashxplem 14468 dmtrclfv 15053 ramcl 17063 0subcat 17879 mat0dimbas0 22462 mavmul0g 22549 txindislem 23631 txhaus 23645 tmdgsum 24093 ust0 24218 ehl0 25441 mbf0 25659 hashxpe 32799 gsumpart 33045 erlval 33250 fracbas 33294 sibf0 34314 lpadlem3 34671 mexval2 35486 poimirlem5 37610 poimirlem10 37615 poimirlem22 37627 poimirlem23 37628 poimirlem26 37631 poimirlem28 37633 0no 43426 0heALT 43774 0funcg2 48893 0funcALT 48897 |
| Copyright terms: Public domain | W3C validator |