Theorem moanimv 2614

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2535

This theorem is referenced by:  2reuswap  3705  2reuswap2  3706  2reu5lem2  3715  2rmoswap  3720  funmo  6497  funcnv  6550  fncnv  6554  isarep2  6571  fnres  6608  mptfnf  6616  fnopabg  6618  fvopab3ig  6925  opabex  7154  fnoprabg  7469  ovidi  7489  ovig  7492  caovmo  7583  zfrep6  7887  oprabexd  7907  oprabex  7908  nqerf  10821  cnextfun  23980  perfdvf  25832  taylf  26296  reuxfrdf  32468  abrexdomjm  32485  abrexdom  37776  modelaxreplem2  45018