Theorem moanimv 2619

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

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

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  ax-7 2009

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

This theorem is referenced by:  2reuswap  3704  2reuswap2  3705  2reu5lem2  3714  2rmoswap  3719  funmo  6508  funcnv  6561  fncnv  6565  isarep2  6582  fnres  6619  mptfnf  6627  fnopabg  6629  fvopab3ig  6937  opabex  7166  fnoprabg  7481  ovidi  7501  ovig  7504  caovmo  7595  zfrep6  7899  oprabexd  7919  oprabex  7920  nqerf  10841  cnextfun  24008  perfdvf  25860  taylf  26324  reuxfrdf  32565  abrexdomjm  32582  abrexdom  37931  modelaxreplem2  45220