Theorem moanimv 2330

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   E*wmo 2267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271

This theorem is referenced by:  2reuswap  3280  2reu5lem2  3284  funmo  5617  funcnv  5661  fncnv  5665  isarep2  5681  fnres  5710  mptfnf  5717  fnopabg  5719  fvopab3ig  5961  opabex  6149  fnoprabg  6411  ovidi  6429  ovig  6432  caovmo  6520  zfrep6  6775  oprabexd  6794  oprabex  6795  nqerf  9354  cnextfun  21010  perfdvf  22735  taylf  23181  2reuswap2  27959  abrexdomjm  27977  abrexdom  31761  2rmoswap  37996