Theorem ndmov 6803

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1481   ∈ wcel 1988  ∅c0 3907   × cxp 5102  dom cdm 5104  (class class class)co 6635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-xp 5110  df-dm 5114  df-iota 5839  df-fv 5884  df-ov 6638

This theorem is referenced by:  ndmovcl  6804  ndmovrcl  6805  ndmovcom  6806  ndmovass  6807  ndmovdistr  6808  om0x  7584  oaabs2  7710  omabs  7712  eceqoveq  7838  elpmi  7861  elmapex  7863  pmresg  7870  pmsspw  7877  cdacomen  8988  cdadom1  8993  cdainf  8999  pwcdadom  9023  addnidpi  9708  adderpq  9763  mulerpq  9764  elixx3g  12173  ndmioo  12187  elfz2  12318  fz0  12341  elfzoel1  12452  elfzoel2  12453  fzoval  12455  fzofi  12756  restsspw  16073  fucbas  16601  fuchom  16602  xpcbas  16799  xpchomfval  16800  xpccofval  16803  restrcl  20942  ssrest  20961  resstopn  20971  iocpnfordt  21000  icomnfordt  21001  nghmfval  22507  isnghm  22508  topnfbey  27295  cvmtop1  31216  cvmtop2  31217  ndmico  39596