![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ndmov | Structured version Visualization version GIF version |
Description: The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.) |
Ref | Expression |
---|---|
ndmov.1 | ⊢ dom 𝐹 = (𝑆 × 𝑆) |
Ref | Expression |
---|---|
ndmov | ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndmov.1 | . 2 ⊢ dom 𝐹 = (𝑆 × 𝑆) | |
2 | ndmovg 6982 | . 2 ⊢ ((dom 𝐹 = (𝑆 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | |
3 | 1, 2 | mpan 708 | 1 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2139 ∅c0 4058 × cxp 5264 dom cdm 5266 (class class class)co 6813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-xp 5272 df-dm 5276 df-iota 6012 df-fv 6057 df-ov 6816 |
This theorem is referenced by: ndmovcl 6984 ndmovrcl 6985 ndmovcom 6986 ndmovass 6987 ndmovdistr 6988 om0x 7768 oaabs2 7894 omabs 7896 eceqoveq 8019 elpmi 8042 elmapex 8044 pmresg 8051 pmsspw 8058 cdacomen 9195 cdadom1 9200 cdainf 9206 pwcdadom 9230 addnidpi 9915 adderpq 9970 mulerpq 9971 elixx3g 12381 ndmioo 12395 elfz2 12526 fz0 12549 elfzoel1 12662 elfzoel2 12663 fzoval 12665 fzofi 12967 restsspw 16294 fucbas 16821 fuchom 16822 xpcbas 17019 xpchomfval 17020 xpccofval 17023 restrcl 21163 ssrest 21182 resstopn 21192 iocpnfordt 21221 icomnfordt 21222 nghmfval 22727 isnghm 22728 topnfbey 27636 cvmtop1 31549 cvmtop2 31550 ndmico 40296 |
Copyright terms: Public domain | W3C validator |