Theorem moimi 2120

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 2119	. 2 |- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
2		moimi.1	. 2 |- ( ph -> ps )
3	1, 2	mpg 1475	1 |- ( E* x ps -> E* x ph )

Syntax hints:   -> wi 4   E*wmo 2056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059

This theorem is referenced by:  moan  2124  moor  2126  mooran1  2127  mooran2  2128  2moex  2141  2euex  2142  2exeu  2147  mosubt  2954  sndisj  4047  disjxsn  4049  mosubopt  4748  fununmo  5325  funcnvsn  5328  nfunsn  5624  th3qlem2  6738  shftfn  11210