MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ndmov Unicode version

Theorem ndmov 6459
Description: The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.)
Hypothesis
Ref Expression
ndmov.1
Assertion
Ref Expression
ndmov

Proof of Theorem ndmov
StepHypRef Expression
1 ndmov.1 . 2
2 ndmovg 6458 . 2
31, 2mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818   c0 3784  X.cxp 5002  domcdm 5004  (class class class)co 6296
This theorem is referenced by:  ndmovcl  6460  ndmovrcl  6461  ndmovcom  6462  ndmovass  6463  ndmovdistr  6464  om0x  7188  oaabs2  7313  omabs  7315  eceqoveq  7435  elpmi  7457  elmapex  7459  pmresg  7466  pmsspw  7473  cdacomen  8582  cdadom1  8587  cdainf  8593  pwcdadom  8617  addnidpi  9300  adderpq  9355  mulerpq  9356  elixx3g  11571  ndmioo  11585  elfz2  11708  fz0  11730  elfzoel1  11827  elfzoel2  11828  fzoval  11830  fzofi  12084  restsspw  14829  fucbas  15329  fuchom  15330  xpcbas  15447  xpchomfval  15448  xpccofval  15451  restrcl  19658  ssrest  19677  resstopn  19687  iocpnfordt  19716  icomnfordt  19717  nghmfval  21229  isnghm  21230  cvmtop1  28705  cvmtop2  28706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-dm 5014  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator