Theorem moanimv 2618

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

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

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 2539

This theorem is referenced by:  2reuswap  3729  2reuswap2  3730  2reu5lem2  3739  2rmoswap  3744  funmo  6551  funmoOLD  6552  funcnv  6605  fncnv  6609  isarep2  6628  fnres  6665  mptfnf  6673  fnopabg  6675  fvopab3ig  6982  opabex  7212  fnoprabg  7530  ovidi  7550  ovig  7553  caovmo  7644  zfrep6  7953  oprabexd  7974  oprabex  7975  nqerf  10944  cnextfun  24002  perfdvf  25856  taylf  26320  reuxfrdf  32472  abrexdomjm  32488  abrexdom  37754  modelaxreplem2  45004