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 1930	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2618	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540

This theorem is referenced by:  2reuswap  3752  2reuswap2  3753  2reu5lem2  3762  2rmoswap  3767  funmo  6581  funmoOLD  6582  funcnv  6635  fncnv  6639  isarep2  6658  fnres  6695  mptfnf  6703  fnopabg  6705  fvopab3ig  7012  opabex  7240  fnoprabg  7556  ovidi  7576  ovig  7579  caovmo  7670  zfrep6  7979  oprabexd  8000  oprabex  8001  nqerf  10970  cnextfun  24072  perfdvf  25938  taylf  26402  reuxfrdf  32510  abrexdomjm  32526  abrexdom  37737  modelaxreplem2  44996