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
|- F/_ x A
rmo3f.2
|- F/_ y A
rmo3f.3
|- F/ y ph
Assertion rmo3f
|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 rmo3f.1
 |-  F/_ x A
2 rmo3f.2
 |-  F/_ y A
3 rmo3f.3
 |-  F/ y ph
4 df-rmo
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
5 sban
 |-  ( [ y / x ] ( x e. A /\ ph ) <-> ( [ y / x ] x e. A /\ [ y / x ] ph ) )
6 1 clelsb1fw
 |-  ( [ y / x ] x e. A <-> y e. A )
7 5 6 bianbi
 |-  ( [ y / x ] ( x e. A /\ ph ) <-> ( y e. A /\ [ y / x ] ph ) )
8 7 anbi2i
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) )
9 an4
 |-  ( ( ( x e. A /\ ph ) /\ ( y e. A /\ [ y / x ] ph ) ) <-> ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
10 ancom
 |-  ( ( x e. A /\ y e. A ) <-> ( y e. A /\ x e. A ) )
11 10 anbi1i
 |-  ( ( ( x e. A /\ y e. A ) /\ ( ph /\ [ y / x ] ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
12 8 9 11 3bitri
 |-  ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) <-> ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) )
13 12 imbi1i
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) )
14 impexp
 |-  ( ( ( ( y e. A /\ x e. A ) /\ ( ph /\ [ y / x ] ph ) ) -> x = y ) <-> ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
15 impexp
 |-  ( ( ( y e. A /\ x e. A ) -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
16 13 14 15 3bitri
 |-  ( ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
17 16 albii
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
18 df-ral
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> A. y ( y e. A -> ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) ) )
19 2 nfcri
 |-  F/ y x e. A
20 19 r19.21
 |-  ( A. y e. A ( x e. A -> ( ( ph /\ [ y / x ] ph ) -> x = y ) ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
21 17 18 20 3bitr2i
 |-  ( A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
22 21 albii
 |-  ( A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
23 19 3 nfan
 |-  F/ y ( x e. A /\ ph )
24 23 mo3
 |-  ( E* x ( x e. A /\ ph ) <-> A. x A. y ( ( ( x e. A /\ ph ) /\ [ y / x ] ( x e. A /\ ph ) ) -> x = y ) )
25 df-ral
 |-  ( A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x ( x e. A -> A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
26 22 24 25 3bitr4i
 |-  ( E* x ( x e. A /\ ph ) <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
27 4 26 bitri
 |-  ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )