Metamath Proof Explorer


Theorem mob2

Description: Consequence of "at most one". (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypothesis moi2.1 x=Aφψ
Assertion mob2 AB*xφφx=Aψ

Proof

Step Hyp Ref Expression
1 moi2.1 x=Aφψ
2 simp3 AB*xφφφ
3 2 1 syl5ibcom AB*xφφx=Aψ
4 nfv xψ
5 4 1 sbhypf y=Ayxφψ
6 5 anbi2d y=Aφyxφφψ
7 eqeq2 y=Ax=yx=A
8 6 7 imbi12d y=Aφyxφx=yφψx=A
9 8 spcgv AByφyxφx=yφψx=A
10 nfs1v xyxφ
11 sbequ12 x=yφyxφ
12 10 11 mo4f *xφxyφyxφx=y
13 sp xyφyxφx=yyφyxφx=y
14 12 13 sylbi *xφyφyxφx=y
15 9 14 impel AB*xφφψx=A
16 15 expd AB*xφφψx=A
17 16 3impia AB*xφφψx=A
18 3 17 impbid AB*xφφx=Aψ