Theorem ndmov 7533

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∅c0 4284   × cxp 5617  dom cdm 5619  (class class class)co 7349

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-dm 5629  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  ndmovcl  7534  ndmovrcl  7535  ndmovcom  7536  ndmovass  7537  ndmovdistr  7538  om0x  8437  oaabs2  8567  omabs  8569  eceqoveq  8749  elpmi  8773  elmapex  8775  pmresg  8797  pmsspw  8804  addnidpi  10795  adderpq  10850  mulerpq  10851  elixx3g  13261  ndmioo  13275  elfz2  13417  fz0  13442  elfzoel1  13560  elfzoel2  13561  fzoval  13563  fzofi  13881  restsspw  17335  fucbas  17870  fuchom  17871  xpcbas  18084  xpchomfval  18085  xpccofval  18088  restrcl  23042  ssrest  23061  resstopn  23071  iocpnfordt  23100  icomnfordt  23101  nghmfval  24608  isnghm  24609  topnfbey  30413  cvmtop1  35237  cvmtop2  35238  ndmico  45549