Metamath Proof Explorer


Theorem dmdbr2

Description: Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr . (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion dmdbr2 A C B C A 𝑀 * B x C B x x A B x A B

Proof

Step Hyp Ref Expression
1 dmdbr A C B C A 𝑀 * B x C B x x A B = x A B
2 chincl x C A C x A C
3 2 ancoms A C x C x A C
4 3 adantlr A C B C x C x A C
5 simplr A C B C x C B C
6 simpr A C B C x C x C
7 inss1 x A x
8 chlub x A C B C x C x A x B x x A B x
9 8 biimpd x A C B C x C x A x B x x A B x
10 7 9 mpani x A C B C x C B x x A B x
11 4 5 6 10 syl3anc A C B C x C B x x A B x
12 simpll A C B C x C A C
13 inss2 x A A
14 chlej1 x A C A C B C x A A x A B A B
15 13 14 mpan2 x A C A C B C x A B A B
16 4 12 5 15 syl3anc A C B C x C x A B A B
17 11 16 jctird A C B C x C B x x A B x x A B A B
18 ssin x A B x x A B A B x A B x A B
19 17 18 syl6ib A C B C x C B x x A B x A B
20 eqss x A B = x A B x A B x A B x A B x A B
21 20 baib x A B x A B x A B = x A B x A B x A B
22 19 21 syl6 A C B C x C B x x A B = x A B x A B x A B
23 22 pm5.74d A C B C x C B x x A B = x A B B x x A B x A B
24 23 ralbidva A C B C x C B x x A B = x A B x C B x x A B x A B
25 1 24 bitrd A C B C A 𝑀 * B x C B x x A B x A B