Metamath Proof Explorer


Theorem ssmd1

Description: Ordering implies the modular pair property. Remark in MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion ssmd1 ACBCABA𝑀B

Proof

Step Hyp Ref Expression
1 inss1 xABxA
2 dfss ABA=AB
3 2 biimpi ABA=AB
4 3 oveq2d ABxA=xAB
5 1 4 sseqtrid ABxABxAB
6 5 a1d ABxBxABxAB
7 6 ralrimivw ABxCxBxABxAB
8 mdbr2 ACBCA𝑀BxCxBxABxAB
9 7 8 imbitrrid ACBCABA𝑀B
10 9 3impia ACBCABA𝑀B