Theorem moanimv 2531

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   E*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  2reuswap  3410  2reu5lem2  3414  funmo  5904  funcnv  5958  fncnv  5962  isarep2  5978  fnres  6007  mptfnf  6015  fnopabg  6017  fvopab3ig  6278  opabex  6483  fnoprabg  6761  ovidi  6779  ovig  6782  caovmo  6871  zfrep6  7134  oprabexd  7155  oprabex  7156  nqerf  9752  cnextfun  21868  perfdvf  23667  taylf  24115  2reuswap2  29328  abrexdomjm  29345  abrexdom  33525  2rmoswap  41184