Theorem moanimv 2519

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 1830	. 2 ⊢ Ⅎ𝑥𝜑
2	1	moanim 2517	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∃*wmo 2459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463

This theorem is referenced by:  2reuswap  3377  2reu5lem2  3381  funmo  5820  funcnv  5872  fncnv  5876  isarep2  5892  fnres  5921  mptfnf  5928  fnopabg  5930  fvopab3ig  6188  opabex  6388  fnoprabg  6659  ovidi  6677  ovig  6680  caovmo  6769  zfrep6  7027  oprabexd  7046  oprabex  7047  nqerf  9631  cnextfun  21678  perfdvf  23473  taylf  23919  2reuswap2  28712  abrexdomjm  28729  abrexdom  32695  2rmoswap  39833