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

Metamath Proof Explorer

Theorem moop2

Description: "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis moop2.1 
|- B e. _V
Assertion moop2 
|- E* x A = <. B , x >.

Proof

Step Hyp Ref Expression
1 moop2.1 
 |-  B e. _V
2 eqtr2 
 |-  ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> <. B , x >. = <. [_ y / x ]_ B , y >. )
3 vex 
 |-  x e. _V
4 1 3 opth 
 |-  ( <. B , x >. = <. [_ y / x ]_ B , y >. <-> ( B = [_ y / x ]_ B /\ x = y ) )
5 4 simprbi 
 |-  ( <. B , x >. = <. [_ y / x ]_ B , y >. -> x = y )
6 2 5 syl 
 |-  ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y )
7 6 gen2 
 |-  A. x A. y ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y )
8 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
9 nfcv 
 |-  F/_ x y
10 8 9 nfop 
 |-  F/_ x <. [_ y / x ]_ B , y >.
11 10 nfeq2 
 |-  F/ x A = <. [_ y / x ]_ B , y >.
12 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
13 id 
 |-  ( x = y -> x = y )
14 12 13 opeq12d 
 |-  ( x = y -> <. B , x >. = <. [_ y / x ]_ B , y >. )
15 14 eqeq2d 
 |-  ( x = y -> ( A = <. B , x >. <-> A = <. [_ y / x ]_ B , y >. ) )
16 11 15 mo4f 
 |-  ( E* x A = <. B , x >. <-> A. x A. y ( ( A = <. B , x >. /\ A = <. [_ y / x ]_ B , y >. ) -> x = y ) )
17 7 16 mpbir 
 |-  E* x A = <. B , x >.