![]() |
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 7542 | . 2 ⊢ ((dom 𝐹 = (𝑆 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅) | |
3 | 1, 2 | mpan 688 | 1 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∅c0 4287 × cxp 5636 dom cdm 5638 (class class class)co 7362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pr 5389 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3406 df-v 3448 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-xp 5644 df-dm 5648 df-iota 6453 df-fv 6509 df-ov 7365 |
This theorem is referenced by: ndmovcl 7544 ndmovrcl 7545 ndmovcom 7546 ndmovass 7547 ndmovdistr 7548 om0x 8470 oaabs2 8600 omabs 8602 eceqoveq 8768 elpmi 8791 elmapex 8793 pmresg 8815 pmsspw 8822 addnidpi 10846 adderpq 10901 mulerpq 10902 elixx3g 13287 ndmioo 13301 elfz2 13441 fz0 13466 elfzoel1 13580 elfzoel2 13581 fzoval 13583 fzofi 13889 restsspw 17327 fucbas 17862 fuchom 17863 fuchomOLD 17864 xpcbas 18080 xpchomfval 18081 xpccofval 18084 restrcl 22545 ssrest 22564 resstopn 22574 iocpnfordt 22603 icomnfordt 22604 nghmfval 24123 isnghm 24124 topnfbey 29476 cvmtop1 33941 cvmtop2 33942 ndmico 43924 |
Copyright terms: Public domain | W3C validator |