Theorem ndmov 7540

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∅c0 4283   × cxp 5620  dom cdm 5622  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  ndmovcl  7541  ndmovrcl  7542  ndmovcom  7543  ndmovass  7544  ndmovdistr  7545  om0x  8444  oaabs2  8575  omabs  8577  eceqoveq  8757  elpmi  8781  elmapex  8783  pmresg  8806  pmsspw  8813  addnidpi  10810  adderpq  10865  mulerpq  10866  elixx3g  13272  ndmioo  13286  elfz2  13428  fz0  13453  elfzoel1  13571  elfzoel2  13572  fzoval  13574  fzofi  13895  restsspw  17349  fucbas  17885  fuchom  17886  xpcbas  18099  xpchomfval  18100  xpccofval  18103  restrcl  23099  ssrest  23118  resstopn  23128  iocpnfordt  23157  icomnfordt  23158  nghmfval  24664  isnghm  24665  topnfbey  30493  cvmtop1  35403  cvmtop2  35404  ndmico  45752