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 528	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2549	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1934	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2620	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540

This theorem is referenced by:  2reuswap  3676  2reuswap2  3677  2reu5lem2  3686  2rmoswap  3691  funmo  6434  funcnv  6487  fncnv  6491  isarep2  6507  fnres  6543  mptfnf  6552  fnopabg  6554  fvopab3ig  6853  opabex  7078  fnoprabg  7375  ovidi  7394  ovig  7397  caovmo  7487  zfrep6  7771  oprabexd  7791  oprabex  7792  nqerf  10617  cnextfun  23123  perfdvf  24972  taylf  25425  reuxfrdf  30740  abrexdomjm  30753  abrexdom  35815