Theorem moanimv 2621

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2540

This theorem is referenced by:  2reuswap  3681  2reuswap2  3682  2reu5lem2  3691  2rmoswap  3696  funmo  6450  funcnv  6503  fncnv  6507  isarep2  6523  fnres  6559  mptfnf  6568  fnopabg  6570  fvopab3ig  6871  opabex  7096  fnoprabg  7397  ovidi  7416  ovig  7419  caovmo  7509  zfrep6  7797  oprabexd  7818  oprabex  7819  nqerf  10686  cnextfun  23215  perfdvf  25067  taylf  25520  reuxfrdf  30839  abrexdomjm  30852  abrexdom  35888