Theorem ndmov 7545

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∅c0 4274   × cxp 5623  dom cdm 5625  (class class class)co 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-dm 5635  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  ndmovcl  7546  ndmovrcl  7547  ndmovcom  7548  ndmovass  7549  ndmovdistr  7550  om0x  8448  oaabs2  8579  omabs  8581  eceqoveq  8763  elpmi  8787  elmapex  8789  pmresg  8812  pmsspw  8819  addnidpi  10818  adderpq  10873  mulerpq  10874  elixx3g  13305  ndmioo  13319  elfz2  13462  fz0  13487  elfzoel1  13605  elfzoel2  13606  fzoval  13608  fzofi  13930  restsspw  17388  fucbas  17924  fuchom  17925  xpcbas  18138  xpchomfval  18139  xpccofval  18142  restrcl  23135  ssrest  23154  resstopn  23164  iocpnfordt  23193  icomnfordt  23194  nghmfval  24700  isnghm  24701  topnfbey  30557  cvmtop1  35461  cvmtop2  35462  ndmico  46015