Metamath Proof Explorer


Theorem rmob

Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypotheses rmoi.b x=Bφψ
rmoi.c x=Cφχ
Assertion rmob *xAφBAψB=CCAχ

Proof

Step Hyp Ref Expression
1 rmoi.b x=Bφψ
2 rmoi.c x=Cφχ
3 df-rmo *xAφ*xxAφ
4 simprl *xxAφBAψBA
5 eleq1 B=CBACA
6 4 5 syl5ibcom *xxAφBAψB=CCA
7 simpl CAχCA
8 7 a1i *xxAφBAψCAχCA
9 4 anim1i *xxAφBAψCABACA
10 simpll *xxAφBAψCA*xxAφ
11 simplr *xxAφBAψCABAψ
12 eleq1 x=BxABA
13 12 1 anbi12d x=BxAφBAψ
14 eleq1 x=CxACA
15 14 2 anbi12d x=CxAφCAχ
16 13 15 mob BACA*xxAφBAψB=CCAχ
17 9 10 11 16 syl3anc *xxAφBAψCAB=CCAχ
18 17 ex *xxAφBAψCAB=CCAχ
19 6 8 18 pm5.21ndd *xxAφBAψB=CCAχ
20 3 19 sylanb *xAφBAψB=CCAχ