Theorem ndmov 7637

Description: The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995.)

Hypothesis

Ref	Expression
ndmov.1	⊢ dom 𝐹 = (𝑆 × 𝑆)

Assertion

Ref	Expression
ndmov	⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅)

Proof of Theorem ndmov

Step	Hyp	Ref	Expression
1		ndmov.1	. 2 ⊢ dom 𝐹 = (𝑆 × 𝑆)
2		ndmovg 7636	. 2 ⊢ ((dom 𝐹 = (𝑆 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅)
3	1, 2	mpan 703	1 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∅c0 4281   × cxp 5656  dom cdm 5658  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-dm 5668  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  ndmovcl  7638  ndmovrcl  7639  ndmovcom  7640  ndmovass  7641  ndmovdistr  7642  om0x  8565  oaabs2  8696  omabs  8698  eceqoveq  8881  elpmi  8904  elmapex  8906  pmresg  8936  pmsspw  8943  addnidpi  11025  adderpq  11080  mulerpq  11081  elixx3g  13529  ndmioo  13543  elfz2  13686  fz0  13712  elfzoel1  13831  elfzoel2  13832  fzoval  13834  fzofi  14157  restsspw  17652  fucbas  18188  fuchom  18189  xpcbas  18402  xpchomfval  18403  xpccofval  18406  restrcl  23530  ssrest  23549  resstopn  23559  iocpnfordt  23588  icomnfordt  23589  nghmfval  25096  isnghm  25097  topnfbey  31127  cvmtop1  36233  cvmtop2  36234  ndmico  46849