Theorem moanimv 2615

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2616 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 529	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2543	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1933	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2614	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃*wmo 2532

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 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534

This theorem is referenced by:  2reuswap  3742  2reuswap2  3743  2reu5lem2  3752  2rmoswap  3757  funmo  6563  funmoOLD  6564  funcnv  6617  fncnv  6621  isarep2  6639  fnres  6677  mptfnf  6685  fnopabg  6687  fvopab3ig  6994  opabex  7224  fnoprabg  7533  ovidi  7553  ovig  7556  caovmo  7646  zfrep6  7943  oprabexd  7964  oprabex  7965  nqerf  10927  cnextfun  23788  perfdvf  25644  taylf  26097  reuxfrdf  31986  abrexdomjm  31999  abrexdom  36901