Theorem ndmov 7551

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∅c0 4273   × cxp 5629  dom cdm 5631  (class class class)co 7367

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-dm 5641  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  ndmovcl  7552  ndmovrcl  7553  ndmovcom  7554  ndmovass  7555  ndmovdistr  7556  om0x  8454  oaabs2  8585  omabs  8587  eceqoveq  8769  elpmi  8793  elmapex  8795  pmresg  8818  pmsspw  8825  addnidpi  10824  adderpq  10879  mulerpq  10880  elixx3g  13311  ndmioo  13325  elfz2  13468  fz0  13493  elfzoel1  13611  elfzoel2  13612  fzoval  13614  fzofi  13936  restsspw  17394  fucbas  17930  fuchom  17931  xpcbas  18144  xpchomfval  18145  xpccofval  18148  restrcl  23122  ssrest  23141  resstopn  23151  iocpnfordt  23180  icomnfordt  23181  nghmfval  24687  isnghm  24688  topnfbey  30539  cvmtop1  35442  cvmtop2  35443  ndmico  45994