Theorem moanimv 2649

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2650 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 537	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2579	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1953	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2648	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃*wmo 2567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569

This theorem is referenced by:  2reuswap  3712  2reuswap2  3713  2reu5lem2  3722  2rmoswap  3727  zfrep6  5243  funmo  6541  funcnv  6594  fncnv  6598  isarep2  6615  fnres  6652  mptfnf  6660  fnopabg  6662  fvopab3ig  6975  opabex  7208  fnoprabg  7523  ovidi  7543  ovig  7546  caovmo  7637  zfrep6OLD  7940  oprabexd  7960  oprabex  7961  nqerf  10903  cnextfun  24178  perfdvf  26019  taylf  26478  reuxfrdf  32743  abrexdomjm  32759  bj-rep  37565  abrexdom  38236  ralmo  38866  modelaxreplem2  45547