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 dom F = S × S
ndmov.5 ¬ S
Assertion ndmovass ¬ A S B S C S A F B F C = A F B F C

Proof

Step Hyp Ref Expression
1 ndmov.1 dom F = S × S
2 ndmov.5 ¬ S
3 1 2 ndmovrcl A F B S A S B S
4 3 anim1i A F B S C S A S B S C S
5 df-3an A S B S C S A S B S C S
6 4 5 sylibr A F B S C S A S B S C S
7 1 ndmov ¬ A F B S C S A F B F C =
8 6 7 nsyl5 ¬ A S B S C S A F B F C =
9 1 2 ndmovrcl B F C S B S C S
10 9 anim2i A S B F C S A S B S C S
11 3anass A S B S C S A S B S C S
12 10 11 sylibr A S B F C S A S B S C S
13 1 ndmov ¬ A S B F C S A F B F C =
14 12 13 nsyl5 ¬ A S B S C S A F B F C =
15 8 14 eqtr4d ¬ A S B S C S A F B F C = A F B F C