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

Metamath Proof Explorer

Theorem mob2

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

Ref Expression
Hypothesis moi2.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion mob2 
|- ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A <-> ps ) )

Proof

Step Hyp Ref Expression
1 moi2.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 simp3 
 |-  ( ( A e. B /\ E* x ph /\ ph ) -> ph )
3 2 1 syl5ibcom 
 |-  ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A -> ps ) )
4 nfv 
 |-  F/ x ps
5 4 1 sbhypf 
 |-  ( y = A -> ( [ y / x ] ph <-> ps ) )
6 5 anbi2d 
 |-  ( y = A -> ( ( ph /\ [ y / x ] ph ) <-> ( ph /\ ps ) ) )
7 eqeq2 
 |-  ( y = A -> ( x = y <-> x = A ) )
8 6 7 imbi12d 
 |-  ( y = A -> ( ( ( ph /\ [ y / x ] ph ) -> x = y ) <-> ( ( ph /\ ps ) -> x = A ) ) )
9 8 spcgv 
 |-  ( A e. B -> ( A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> ( ( ph /\ ps ) -> x = A ) ) )
10 nfs1v 
 |-  F/ x [ y / x ] ph
11 sbequ12 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )
12 10 11 mo4f 
 |-  ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
13 sp 
 |-  ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
14 12 13 sylbi 
 |-  ( E* x ph -> A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
15 9 14 impel 
 |-  ( ( A e. B /\ E* x ph ) -> ( ( ph /\ ps ) -> x = A ) )
16 15 expd 
 |-  ( ( A e. B /\ E* x ph ) -> ( ph -> ( ps -> x = A ) ) )
17 16 3impia 
 |-  ( ( A e. B /\ E* x ph /\ ph ) -> ( ps -> x = A ) )
18 3 17 impbid 
 |-  ( ( A e. B /\ E* x ph /\ ph ) -> ( x = A <-> ps ) )