Theorem moim 2519

Description: "At most one" reverses implication. (Contributed by NM, 22-Apr-1995.)

Assertion

Ref	Expression
moim	|- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )

Proof of Theorem moim

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imim1 83	. . . 4 |- ( ( ph -> ps ) -> ( ( ps -> x = y ) -> ( ph -> x = y ) ) )
2	1	al2imi 1743	. . 3 |- ( A. x ( ph -> ps ) -> ( A. x ( ps -> x = y ) -> A. x ( ph -> x = y ) ) )
3	2	eximdv 1846	. 2 |- ( A. x ( ph -> ps ) -> ( E. y A. x ( ps -> x = y ) -> E. y A. x ( ph -> x = y ) ) )
4		mo2v 2477	. 2 |- ( E* x ps <-> E. y A. x ( ps -> x = y ) )
5		mo2v 2477	. 2 |- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
6	3, 4, 5	3imtr4g 285	1 |- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )

Syntax hints:   -> wi 4   A.wal 1481   E.wex 1704   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  moimi  2520  euimmo  2522  moexex  2541  rmoim  3407  rmoimi2  3409  disjss1  4626  disjss3  4652  reusv1OLD  4867  funmo  5904  brdom6disj  9354  uptx  21428  taylf  24115  moimd  29326  ssrmo  29334  funressnfv  41208