Metamath Proof Explorer


Theorem rmo4

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by NM, 16-Jun-2017)

Ref Expression
Hypothesis rmo4.1 x=yφψ
Assertion rmo4 *xAφxAyAφψx=y

Proof

Step Hyp Ref Expression
1 rmo4.1 x=yφψ
2 df-rmo *xAφ*xxAφ
3 an4 xAφyAψxAyAφψ
4 ancom xAyAyAxA
5 3 4 bianbi xAφyAψyAxAφψ
6 5 imbi1i xAφyAψx=yyAxAφψx=y
7 impexp yAxAφψx=yyAxAφψx=y
8 impexp yAxAφψx=yyAxAφψx=y
9 6 7 8 3bitri xAφyAψx=yyAxAφψx=y
10 9 albii yxAφyAψx=yyyAxAφψx=y
11 df-ral yAxAφψx=yyyAxAφψx=y
12 r19.21v yAxAφψx=yxAyAφψx=y
13 10 11 12 3bitr2i yxAφyAψx=yxAyAφψx=y
14 13 albii xyxAφyAψx=yxxAyAφψx=y
15 eleq1w x=yxAyA
16 15 1 anbi12d x=yxAφyAψ
17 16 mo4 *xxAφxyxAφyAψx=y
18 df-ral xAyAφψx=yxxAyAφψx=y
19 14 17 18 3bitr4i *xxAφxAyAφψx=y
20 2 19 bitri *xAφxAyAφψx=y