Theorem ndmov 7594

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 7593	. 2 ⊢ ((dom 𝐹 = (𝑆 × 𝑆) ∧ ¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝐴𝐹𝐵) = ∅)
3	1, 2	mpan 702	1 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∅c0 4286   × cxp 5659  dom cdm 5661  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-dm 5671  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  ndmovcl  7595  ndmovrcl  7596  ndmovcom  7597  ndmovass  7598  ndmovdistr  7599  om0x  8500  oaabs2  8631  omabs  8633  eceqoveq  8816  elpmi  8839  elmapex  8841  pmresg  8864  pmsspw  8871  addnidpi  10881  adderpq  10936  mulerpq  10937  elixx3g  13380  ndmioo  13394  elfz2  13537  fz0  13562  elfzoel1  13681  elfzoel2  13682  fzoval  13684  fzofi  14006  restsspw  17479  fucbas  18015  fuchom  18016  xpcbas  18229  xpchomfval  18230  xpccofval  18233  restrcl  23314  ssrest  23333  resstopn  23343  iocpnfordt  23372  icomnfordt  23373  nghmfval  24879  isnghm  24880  topnfbey  30820  cvmtop1  35752  cvmtop2  35753  ndmico  46300