Theorem ndmov 7543

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∅c0 4287   × cxp 5636  dom cdm 5638  (class class class)co 7362

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-dm 5648  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  ndmovcl  7544  ndmovrcl  7545  ndmovcom  7546  ndmovass  7547  ndmovdistr  7548  om0x  8470  oaabs2  8600  omabs  8602  eceqoveq  8768  elpmi  8791  elmapex  8793  pmresg  8815  pmsspw  8822  addnidpi  10846  adderpq  10901  mulerpq  10902  elixx3g  13287  ndmioo  13301  elfz2  13441  fz0  13466  elfzoel1  13580  elfzoel2  13581  fzoval  13583  fzofi  13889  restsspw  17327  fucbas  17862  fuchom  17863  fuchomOLD  17864  xpcbas  18080  xpchomfval  18081  xpccofval  18084  restrcl  22545  ssrest  22564  resstopn  22574  iocpnfordt  22603  icomnfordt  22604  nghmfval  24123  isnghm  24124  topnfbey  29476  cvmtop1  33941  cvmtop2  33942  ndmico  43924