This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rmo4f

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by Thierry Arnoux, 11-Oct-2016) (Revised by Thierry Arnoux, 8-Mar-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo4f.1 
|- F/_ x A
rmo4f.2 
|- F/_ y A
rmo4f.3 
|- F/ x ps
rmo4f.4 
|- ( x = y -> ( ph <-> ps ) )
Assertion rmo4f 
|- ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 rmo4f.1 
 |-  F/_ x A
2 rmo4f.2 
 |-  F/_ y A
3 rmo4f.3 
 |-  F/ x ps
4 rmo4f.4 
 |-  ( x = y -> ( ph <-> ps ) )
5 nfv 
 |-  F/ y ph
6 1 2 5 rmo3f 
 |-  ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) )
7 3 4 sbiev 
 |-  ( [ y / x ] ph <-> ps )
8 7 anbi2i 
 |-  ( ( ph /\ [ y / x ] ph ) <-> ( ph /\ ps ) )
9 8 imbi1i 
 |-  ( ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ ps ) -> x = y ) )
10 9 2ralbii 
 |-  ( A. x e. A A. y e. A ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )
11 6 10 bitri 
 |-  ( E* x e. A ph <-> A. x e. A A. y e. A ( ( ph /\ ps ) -> x = y ) )