Theorem ndmov 7531

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∅c0 4281   × cxp 5629  dom cdm 5631  (class class class)co 7350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-xp 5637  df-dm 5641  df-iota 6444  df-fv 6500  df-ov 7353

This theorem is referenced by:  ndmovcl  7532  ndmovrcl  7533  ndmovcom  7534  ndmovass  7535  ndmovdistr  7536  om0x  8433  oaabs2  8563  omabs  8565  eceqoveq  8695  elpmi  8718  elmapex  8720  pmresg  8742  pmsspw  8749  addnidpi  10771  adderpq  10826  mulerpq  10827  elixx3g  13207  ndmioo  13221  elfz2  13361  fz0  13386  elfzoel1  13500  elfzoel2  13501  fzoval  13503  fzofi  13809  restsspw  17249  fucbas  17784  fuchom  17785  fuchomOLD  17786  xpcbas  18002  xpchomfval  18003  xpccofval  18006  restrcl  22436  ssrest  22455  resstopn  22465  iocpnfordt  22494  icomnfordt  22495  nghmfval  24014  isnghm  24015  topnfbey  29218  cvmtop1  33634  cvmtop2  33635  ndmico  43595