Theorem moanimv 2131

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   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:  mosubt  2957  2reuswapdc  2984  2rmorex  2986  mosubopt  4758  funmo  5305  funcnv  5354  fncnv  5359  isarep2  5380  fnres  5412  fnopabg  5419  fvopab3ig  5676  opabex  5831  fnoprabg  6069  ovidi  6087  ovig  6090  oprabexd  6235  oprabex  6236  th3qcor  6749  dvfgg  15275