Theorem moanimv 2616

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2617 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 528	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2546	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1931	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2615	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃*wmo 2535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2537

This theorem is referenced by:  2reuswap  3701  2reuswap2  3702  2reu5lem2  3711  2rmoswap  3716  funmo  6504  funcnv  6557  fncnv  6561  isarep2  6578  fnres  6615  mptfnf  6623  fnopabg  6625  fvopab3ig  6933  opabex  7162  fnoprabg  7477  ovidi  7497  ovig  7500  caovmo  7591  zfrep6  7895  oprabexd  7915  oprabex  7916  nqerf  10830  cnextfun  23982  perfdvf  25834  taylf  26298  reuxfrdf  32474  abrexdomjm  32491  abrexdom  37793  modelaxreplem2  45099