Metamath Proof Explorer


Theorem mdbr2

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

Ref Expression
Assertion mdbr2 A C B C A 𝑀 B x C x B x A B x A B

Proof

Step Hyp Ref Expression
1 mdbr A C B C A 𝑀 B x C x B x A B = x A B
2 chub1 x C A C x x A
3 2 ancoms A C x C x x A
4 iba x B x x A x x A x B
5 ssin x x A x B x x A B
6 4 5 bitrdi x B x x A x x A B
7 3 6 syl5ibcom A C x C x B x x A B
8 chub2 A C x C A x A
9 8 ssrind A C x C A B x A B
10 7 9 jctird A C x C x B x x A B A B x A B
11 10 adantlr A C B C x C x B x x A B A B x A B
12 simpr A C B C x C x C
13 chincl A C B C A B C
14 13 adantr A C B C x C A B C
15 chjcl x C A C x A C
16 15 ancoms A C x C x A C
17 chincl x A C B C x A B C
18 16 17 sylan A C x C B C x A B C
19 18 an32s A C B C x C x A B C
20 chlub x C A B C x A B C x x A B A B x A B x A B x A B
21 12 14 19 20 syl3anc A C B C x C x x A B A B x A B x A B x A B
22 11 21 sylibd A C B C x C x B x A B x A B
23 eqss x A B = x A B x A B x A B x A B x A B
24 23 rbaib x A B x A B x A B = x A B x A B x A B
25 22 24 syl6 A C B C x C x B x A B = x A B x A B x A B
26 25 pm5.74d A C B C x C x B x A B = x A B x B x A B x A B
27 26 ralbidva A C B C x C x B x A B = x A B x C x B x A B x A B
28 1 27 bitrd A C B C A 𝑀 B x C x B x A B x A B