Theorem moanimv 2371

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   E*wmo 2311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-eu 2314  df-mo 2315

This theorem is referenced by:  2reuswap  3254  2reu5lem2  3258  funmo  5617  funcnv  5665  fncnv  5669  isarep2  5685  fnres  5714  mptfnf  5721  fnopabg  5723  fvopab3ig  5968  opabex  6159  fnoprabg  6424  ovidi  6442  ovig  6445  caovmo  6533  zfrep6  6788  oprabexd  6807  oprabex  6808  nqerf  9381  cnextfun  21128  perfdvf  22907  taylf  23365  2reuswap2  28173  abrexdomjm  28190  abrexdom  32102  2rmoswap  38643