Theorem ndmov 7591

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∅c0 4308   × cxp 5652  dom cdm 5654  (class class class)co 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-dm 5664  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  ndmovcl  7592  ndmovrcl  7593  ndmovcom  7594  ndmovass  7595  ndmovdistr  7596  om0x  8531  oaabs2  8661  omabs  8663  eceqoveq  8836  elpmi  8860  elmapex  8862  pmresg  8884  pmsspw  8891  addnidpi  10915  adderpq  10970  mulerpq  10971  elixx3g  13375  ndmioo  13389  elfz2  13531  fz0  13556  elfzoel1  13674  elfzoel2  13675  fzoval  13677  fzofi  13992  restsspw  17445  fucbas  17976  fuchom  17977  xpcbas  18190  xpchomfval  18191  xpccofval  18194  restrcl  23095  ssrest  23114  resstopn  23124  iocpnfordt  23153  icomnfordt  23154  nghmfval  24661  isnghm  24662  topnfbey  30450  cvmtop1  35282  cvmtop2  35283  ndmico  45593