MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ndmovrcl Structured version   Visualization version   GIF version

Theorem ndmovrcl 7150
Description: Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.)
Hypotheses
Ref Expression
ndmov.1 dom 𝐹 = (𝑆 × 𝑆)
ndmovrcl.3 ¬ ∅ ∈ 𝑆
Assertion
Ref Expression
ndmovrcl ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴𝑆𝐵𝑆))

Proof of Theorem ndmovrcl
StepHypRef Expression
1 ndmovrcl.3 . . 3 ¬ ∅ ∈ 𝑆
2 ndmov.1 . . . . 5 dom 𝐹 = (𝑆 × 𝑆)
32ndmov 7148 . . . 4 (¬ (𝐴𝑆𝐵𝑆) → (𝐴𝐹𝐵) = ∅)
43eleq1d 2850 . . 3 (¬ (𝐴𝑆𝐵𝑆) → ((𝐴𝐹𝐵) ∈ 𝑆 ↔ ∅ ∈ 𝑆))
51, 4mtbiri 319 . 2 (¬ (𝐴𝑆𝐵𝑆) → ¬ (𝐴𝐹𝐵) ∈ 𝑆)
65con4i 114 1 ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴𝑆𝐵𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 387   = wceq 1507  wcel 2050  c0 4178   × cxp 5405  dom cdm 5407  (class class class)co 6976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-xp 5413  df-dm 5417  df-iota 6152  df-fv 6196  df-ov 6979
This theorem is referenced by:  ndmovass  7152  ndmovdistr  7153  ndmovord  7154  ndmovordi  7155  caovmo  7201  brecop2  8191  eceqoveq  8202  addcanpi  10119  mulcanpi  10120  ordpipq  10162  recmulnq  10184  recclnq  10186  ltexnq  10195  nsmallnq  10197  ltbtwnnq  10198  prlem934  10253  ltaddpr  10254  ltaddpr2  10255  ltexprlem2  10257  ltexprlem3  10258  ltexprlem4  10259  ltexprlem6  10261  ltexprlem7  10262  addcanpr  10266  prlem936  10267  mappsrpr  10328
  Copyright terms: Public domain W3C validator