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

Metamath Proof Explorer

Theorem rmo2

Description: Alternate definition of restricted "at most one". Note that E* x e. A ph is not equivalent to E. y e. A A. x e. A ( ph -> x = y ) (in analogy to reu6 ); to see this, let A be the empty set. However, one direction of this pattern holds; see rmo2i . (Contributed by NM, 17-Jun-2017)

Ref Expression
Hypothesis rmo2.1 
|- F/ y ph
Assertion rmo2 
|- ( E* x e. A ph <-> E. y A. x e. A ( ph -> x = y ) )

Proof

Step Hyp Ref Expression
1 rmo2.1 
 |-  F/ y ph
2 df-rmo 
 |-  ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
3 nfv 
 |-  F/ y x e. A
4 3 1 nfan 
 |-  F/ y ( x e. A /\ ph )
5 4 mof 
 |-  ( E* x ( x e. A /\ ph ) <-> E. y A. x ( ( x e. A /\ ph ) -> x = y ) )
6 impexp 
 |-  ( ( ( x e. A /\ ph ) -> x = y ) <-> ( x e. A -> ( ph -> x = y ) ) )
7 6 albii 
 |-  ( A. x ( ( x e. A /\ ph ) -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
8 df-ral 
 |-  ( A. x e. A ( ph -> x = y ) <-> A. x ( x e. A -> ( ph -> x = y ) ) )
9 7 8 bitr4i 
 |-  ( A. x ( ( x e. A /\ ph ) -> x = y ) <-> A. x e. A ( ph -> x = y ) )
10 9 exbii 
 |-  ( E. y A. x ( ( x e. A /\ ph ) -> x = y ) <-> E. y A. x e. A ( ph -> x = y ) )
11 2 5 10 3bitri 
 |-  ( E* x e. A ph <-> E. y A. x e. A ( ph -> x = y ) )