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

Theorem ndmov 6358
Description: The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.)
Hypothesis
Ref Expression
ndmov.1  |-  dom  F  =  ( S  X.  S )
Assertion
Ref Expression
ndmov  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( A F B )  =  (/) )

Proof of Theorem ndmov
StepHypRef Expression
1 ndmov.1 . 2  |-  dom  F  =  ( S  X.  S )
2 ndmovg 6357 . 2  |-  ( ( dom  F  =  ( S  X.  S )  /\  -.  ( A  e.  S  /\  B  e.  S ) )  -> 
( A F B )  =  (/) )
31, 2mpan 670 1  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( A F B )  =  (/) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   (/)c0 3746    X. cxp 4947   dom cdm 4949  (class class class)co 6201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-xp 4955  df-dm 4959  df-iota 5490  df-fv 5535  df-ov 6204
This theorem is referenced by:  ndmovcl  6359  ndmovrcl  6360  ndmovcom  6361  ndmovass  6362  ndmovdistr  6363  om0x  7070  oaabs2  7195  omabs  7197  eceqoveq  7316  elpmi  7342  elmapex  7344  pmresg  7351  pmsspw  7358  cdacomen  8462  cdadom1  8467  cdainf  8473  pwcdadom  8497  addnidpi  9182  adderpq  9237  mulerpq  9238  elixx3g  11425  ndmioo  11439  elfz2  11562  fz0  11583  elfzoel1  11669  elfzoel2  11670  fzoval  11672  fzofi  11914  restsspw  14490  fucbas  14990  fuchom  14991  xpcbas  15108  xpchomfval  15109  xpccofval  15112  restrcl  18894  ssrest  18913  resstopn  18923  iocpnfordt  18952  icomnfordt  18953  nghmfval  20434  isnghm  20435  cvmtop1  27294  cvmtop2  27295
  Copyright terms: Public domain W3C validator