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

Theorem ndmovrcl 6460
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  F  =  ( S  X.  S )
ndmovrcl.3  |-  -.  (/)  e.  S
Assertion
Ref Expression
ndmovrcl  |-  ( ( A F B )  e.  S  ->  ( A  e.  S  /\  B  e.  S )
)

Proof of Theorem ndmovrcl
StepHypRef Expression
1 ndmovrcl.3 . . 3  |-  -.  (/)  e.  S
2 ndmov.1 . . . . 5  |-  dom  F  =  ( S  X.  S )
32ndmov 6458 . . . 4  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( A F B )  =  (/) )
43eleq1d 2526 . . 3  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( ( A F B )  e.  S  <->  (/)  e.  S ) )
51, 4mtbiri 303 . 2  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  -.  ( A F B )  e.  S )
65con4i 130 1  |-  ( ( A F B )  e.  S  ->  ( A  e.  S  /\  B  e.  S )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   (/)c0 3793    X. cxp 5006   dom cdm 5008  (class class class)co 6296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-xp 5014  df-dm 5018  df-iota 5557  df-fv 5602  df-ov 6299
This theorem is referenced by:  ndmovass  6462  ndmovdistr  6463  ndmovord  6464  ndmovordi  6465  caovmo  6511  brecop2  7423  eceqoveq  7434  addcanpi  9294  mulcanpi  9295  ordpipq  9337  recmulnq  9359  recclnq  9361  ltexnq  9370  nsmallnq  9372  ltbtwnnq  9373  prlem934  9428  ltaddpr  9429  ltaddpr2  9430  ltexprlem2  9432  ltexprlem3  9433  ltexprlem4  9434  ltexprlem6  9436  ltexprlem7  9437  addcanpr  9441  prlem936  9442  mappsrpr  9502
  Copyright terms: Public domain W3C validator