Theorem moanimv 2129

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

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058

This theorem is referenced by:  mosubt  2950  2reuswapdc  2977  2rmorex  2979  mosubopt  4740  funmo  5286  funcnv  5335  fncnv  5340  isarep2  5361  fnres  5392  fnopabg  5399  fvopab3ig  5653  opabex  5808  fnoprabg  6046  ovidi  6064  ovig  6067  oprabexd  6212  oprabex  6213  th3qcor  6726  dvfgg  15160