Theorem moanimv 1468

Description: Introduction of a conjunct into "at most one" quantifier.

Assertion

Ref	Expression
moanimv	|- (E*x(ph /\ ps) <-> (ph -> E*xps))

Distinct variable group:   ph,x

Proof of Theorem moanimv

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 |- (ph -> A.xph)
2	1	moanim 1466	1 |- (E*x(ph /\ ps) <-> (ph -> E*xps))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  E*wmo 1420

This theorem is referenced by:  2reuswap 1983  funcnv 3662  fncnv 3666  isarep2 3684  opabex 3715  zfrep6 3721  fnopabg 3722  fvopab3ig 3889  fnoprabg 4072  oprabex 4079  oprabvalig 4084  th3qcor 4457  oprabexd 11813  abrexdom 11826

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422

Copyright terms: Public domain