Theorem moanimv 2155

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 1576	. 2 |- F/ x ph
2	1	moanim 2154	1 |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083

This theorem is referenced by:  mosubt  2983  2reuswapdc  3010  2rmorex  3012  mosubopt  4791  funmo  5341  funcnv  5391  fncnv  5396  isarep2  5417  fnres  5449  fnopabg  5456  fvopab3ig  5720  opabex  5877  fnoprabg  6121  ovidi  6139  ovig  6142  oprabexd  6288  oprabex  6289  th3qcor  6807  dvfgg  15411