Theorem moanimv 2612

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃*wmo 2531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533

This theorem is referenced by:  2reuswap  3717  2reuswap2  3718  2reu5lem2  3727  2rmoswap  3732  funmo  6531  funmoOLD  6532  funcnv  6585  fncnv  6589  isarep2  6608  fnres  6645  mptfnf  6653  fnopabg  6655  fvopab3ig  6964  opabex  7194  fnoprabg  7512  ovidi  7532  ovig  7535  caovmo  7626  zfrep6  7933  oprabexd  7954  oprabex  7955  nqerf  10883  cnextfun  23951  perfdvf  25804  taylf  26268  reuxfrdf  32420  abrexdomjm  32436  abrexdom  37724  modelaxreplem2  44969