Theorem moanimv 2078

Description: Introduction of a conjunct into at-most-one quantifier. (Contributed by NM, 23-Mar-1995.)

Assertion

Ref	Expression
moanimv	|- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem moanimv

Step	Hyp	Ref	Expression
1		nfv 1505	. 2 |- F/ x ph
2	1	moanim 2077	1 |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   E*wmo 2004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007

This theorem is referenced by:  mosubt  2885  2reuswapdc  2912  2rmorex  2914  mosubopt  4644  funmo  5178  funcnv  5224  fncnv  5229  isarep2  5250  fnres  5279  fnopabg  5286  fvopab3ig  5535  opabex  5684  fnoprabg  5912  ovidi  5929  ovig  5932  oprabexd  6065  oprabex  6066  th3qcor  6573  dvfgg  13004