Theorem moanimv 2680

Description: Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)

Assertion

Ref	Expression
moanimv	⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem moanimv

Step	Hyp	Ref	Expression
1		nfv 1995	. 2 ⊢ Ⅎ𝑥𝜑
2	1	moanim 2678	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382  ∃*wmo 2619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-nf 1858  df-eu 2622  df-mo 2623

This theorem is referenced by:  2reuswap  3562  2reu5lem2  3566  funmo  6047  funcnv  6098  fncnv  6102  isarep2  6118  fnres  6147  mptfnf  6155  fnopabg  6157  fvopab3ig  6420  opabex  6627  fnoprabg  6908  ovidi  6926  ovig  6929  caovmo  7018  zfrep6  7281  oprabexd  7302  oprabex  7303  nqerf  9954  cnextfun  22088  perfdvf  23887  taylf  24335  2reuswap2  29667  abrexdomjm  29683  abrexdom  33857  2rmoswap  41704