Theorem moanimv 2681

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃*wmo 2596

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 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598

This theorem is referenced by:  2reuswap  3685  2reuswap2  3686  2reu5lem2  3695  2rmoswap  3700  funmo  6340  funcnv  6393  fncnv  6397  isarep2  6413  fnres  6446  mptfnf  6455  fnopabg  6457  fvopab3ig  6741  opabex  6960  fnoprabg  7254  ovidi  7272  ovig  7275  caovmo  7365  zfrep6  7638  oprabexd  7658  oprabex  7659  nqerf  10341  cnextfun  22669  perfdvf  24506  taylf  24956  reuxfrdf  30262  abrexdomjm  30275  abrexdom  35168