Theorem ndmov 7617

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∅c0 4339   × cxp 5687  dom cdm 5689  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-xp 5695  df-dm 5699  df-iota 6516  df-fv 6571  df-ov 7434

This theorem is referenced by:  ndmovcl  7618  ndmovrcl  7619  ndmovcom  7620  ndmovass  7621  ndmovdistr  7622  om0x  8556  oaabs2  8686  omabs  8688  eceqoveq  8861  elpmi  8885  elmapex  8887  pmresg  8909  pmsspw  8916  addnidpi  10939  adderpq  10994  mulerpq  10995  elixx3g  13397  ndmioo  13411  elfz2  13551  fz0  13576  elfzoel1  13694  elfzoel2  13695  fzoval  13697  fzofi  14012  restsspw  17478  fucbas  18016  fuchom  18017  fuchomOLD  18018  xpcbas  18234  xpchomfval  18235  xpccofval  18238  restrcl  23181  ssrest  23200  resstopn  23210  iocpnfordt  23239  icomnfordt  23240  nghmfval  24759  isnghm  24760  topnfbey  30498  cvmtop1  35245  cvmtop2  35246  ndmico  45519