Metamath Proof Explorer


Theorem rmo3f

Description: Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo3f.1 _xA
rmo3f.2 _yA
rmo3f.3 yφ
Assertion rmo3f *xAφxAyAφyxφx=y

Proof

Step Hyp Ref Expression
1 rmo3f.1 _xA
2 rmo3f.2 _yA
3 rmo3f.3 yφ
4 df-rmo *xAφ*xxAφ
5 sban yxxAφyxxAyxφ
6 1 clelsb1fw yxxAyA
7 5 6 bianbi yxxAφyAyxφ
8 7 anbi2i xAφyxxAφxAφyAyxφ
9 an4 xAφyAyxφxAyAφyxφ
10 ancom xAyAyAxA
11 10 anbi1i xAyAφyxφyAxAφyxφ
12 8 9 11 3bitri xAφyxxAφyAxAφyxφ
13 12 imbi1i xAφyxxAφx=yyAxAφyxφx=y
14 impexp yAxAφyxφx=yyAxAφyxφx=y
15 impexp yAxAφyxφx=yyAxAφyxφx=y
16 13 14 15 3bitri xAφyxxAφx=yyAxAφyxφx=y
17 16 albii yxAφyxxAφx=yyyAxAφyxφx=y
18 df-ral yAxAφyxφx=yyyAxAφyxφx=y
19 2 nfcri yxA
20 19 r19.21 yAxAφyxφx=yxAyAφyxφx=y
21 17 18 20 3bitr2i yxAφyxxAφx=yxAyAφyxφx=y
22 21 albii xyxAφyxxAφx=yxxAyAφyxφx=y
23 19 3 nfan yxAφ
24 23 mo3 *xxAφxyxAφyxxAφx=y
25 df-ral xAyAφyxφx=yxxAyAφyxφx=y
26 22 24 25 3bitr4i *xxAφxAyAφyxφx=y
27 4 26 bitri *xAφxAyAφyxφx=y