Theorem moanimv 2704

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∃*wmo 2620

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 1970

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622

This theorem is referenced by:  2reuswap  3739  2reuswap2  3740  2reu5lem2  3749  2rmoswap  3754  funmo  6373  funcnv  6425  fncnv  6429  isarep2  6445  fnres  6476  mptfnf  6485  fnopabg  6487  fvopab3ig  6766  opabex  6985  fnoprabg  7277  ovidi  7295  ovig  7298  caovmo  7387  zfrep6  7658  oprabexd  7678  oprabex  7679  nqerf  10354  cnextfun  22674  perfdvf  24503  taylf  24951  reuxfrdf  30257  abrexdomjm  30269  abrexdom  35007