Theorem moanimv 2614

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2615 requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023.)

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem moanimv

Step	Hyp	Ref	Expression
1		ibar 529	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2542	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1933	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2613	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃*wmo 2531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533

This theorem is referenced by:  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2rmoswap  3722  funmo  6521  funmoOLD  6522  funcnv  6575  fncnv  6579  isarep2  6597  fnres  6633  mptfnf  6641  fnopabg  6643  fvopab3ig  6949  opabex  7175  fnoprabg  7484  ovidi  7503  ovig  7506  caovmo  7596  zfrep6  7892  oprabexd  7913  oprabex  7914  nqerf  10875  cnextfun  23452  perfdvf  25304  taylf  25757  reuxfrdf  31483  abrexdomjm  31497  abrexdom  36262