Theorem moanimv 2644

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2645 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 538	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2574	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 488	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1962	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2643	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃*wmo 2562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564

This theorem is used by:  2reuswap  3703  2reuswap2  3704  2reu5lem2  3713  2rmoswap  3718  zfrep6  5241  funmo  6555  funcnv  6610  fncnv  6614  isarep2  6630  fnres  6667  mptfnf  6675  fnopabg  6677  fvopab3ig  6990  opabex  7227  fnoprabg  7544  ovidi  7564  ovig  7567  caovmo  7659  zfrep6OLD  7968  oprabexd  7988  oprabex  7989  nqerf  11019  cnextfun  24389  perfdvf  26229  taylf  26694  reuxfrdf  33135  abrexdomjm  33151  bj-rep  38082  abrexdom  38758  ralmo  39386  modelaxreplem2  46063