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

Theorem ndmovrcl 6093
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 6091 . . . 4  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( A F B )  =  (/) )
43eleq1d 2424 . . 3  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  ( ( A F B )  e.  S  <->  (/)  e.  S ) )
51, 4mtbiri 294 . 2  |-  ( -.  ( A  e.  S  /\  B  e.  S
)  ->  -.  ( A F B )  e.  S )
65con4i 122 1  |-  ( ( A F B )  e.  S  ->  ( A  e.  S  /\  B  e.  S )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710   (/)c0 3531    X. cxp 4769   dom cdm 4771  (class class class)co 5945
This theorem is referenced by:  ndmovass  6095  ndmovdistr  6096  ndmovord  6097  ndmovordi  6098  caovmo  6144  brecop2  6840  eceqoveq  6851  addcanpi  8613  mulcanpi  8614  ordpipq  8656  recmulnq  8678  recclnq  8680  ltexnq  8689  nsmallnq  8691  ltbtwnnq  8692  prlem934  8747  ltaddpr  8748  ltaddpr2  8749  ltexprlem2  8751  ltexprlem3  8752  ltexprlem4  8753  ltexprlem6  8755  ltexprlem7  8756  addcanpr  8760  prlem936  8761  mappsrpr  8820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-xp 4777  df-dm 4781  df-iota 5301  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator