Metamath Proof Explorer


Theorem ndmovass

Description: Any operation is associative outside its domain, if the domain doesn't contain the empty set. (Contributed by NM, 24-Aug-1995)

Ref Expression
Hypotheses ndmov.1 domF=S×S
ndmov.5 ¬S
Assertion ndmovass ¬ASBSCSAFBFC=AFBFC

Proof

Step Hyp Ref Expression
1 ndmov.1 domF=S×S
2 ndmov.5 ¬S
3 1 2 ndmovrcl AFBSASBS
4 3 anim1i AFBSCSASBSCS
5 df-3an ASBSCSASBSCS
6 4 5 sylibr AFBSCSASBSCS
7 1 ndmov ¬AFBSCSAFBFC=
8 6 7 nsyl5 ¬ASBSCSAFBFC=
9 1 2 ndmovrcl BFCSBSCS
10 9 anim2i ASBFCSASBSCS
11 3anass ASBSCSASBSCS
12 10 11 sylibr ASBFCSASBSCS
13 1 ndmov ¬ASBFCSAFBFC=
14 12 13 nsyl5 ¬ASBSCSAFBFC=
15 8 14 eqtr4d ¬ASBSCSAFBFC=AFBFC