Theorem moanimv 2620

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2621 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 2550	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1932	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2619	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  2reuswap  3706  2reuswap2  3707  2reu5lem2  3716  2rmoswap  3721  funmo  6516  funcnv  6569  fncnv  6573  isarep2  6590  fnres  6627  mptfnf  6635  fnopabg  6637  fvopab3ig  6945  opabex  7176  fnoprabg  7491  ovidi  7511  ovig  7514  caovmo  7605  zfrep6  7909  oprabexd  7929  oprabex  7930  nqerf  10853  cnextfun  24020  perfdvf  25872  taylf  26336  reuxfrdf  32576  abrexdomjm  32593  bj-rep  37318  abrexdom  37978  ralmo  38608  modelaxreplem2  45332