Theorem moimi 2359

Description: "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)

Hypothesis

Ref	Expression
moimi.1	|- ( ph -> ps )

Assertion

Ref	Expression
moimi	|- ( E* x ps -> E* x ph )

Proof of Theorem moimi

Step	Hyp	Ref	Expression
1		moim 2358	. 2 |- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
2		moimi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1681	1 |- ( E* x ps -> E* x ph )

Syntax hints:   -> wi 4   E*wmo 2310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-12 1943

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678  df-eu 2313  df-mo 2314

This theorem is referenced by:  morimOLD  2360  moan  2363  moor  2365  mooran1  2366  mooran2  2367  moaneu  2372  2moex  2382  2euex  2383  2exeu  2388  sndisj  4407  disjxsn  4409  fununmo  5643  funcnvsn  5645  nfunsn  5918  caovmo  6532  iunmapdisj  8479  brdom3  8981  brdom5  8982  brdom4  8983  nqerf  9380  shftfn  13184  2ndcdisj2  20520  plyexmo  23314  ajfuni  26549  funadj  27587  cnlnadjeui  27778