Theorem moanimv 2623

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543

This theorem is referenced by:  2reuswap  3694  2reuswap2  3695  2reu5lem2  3704  2rmoswap  3709  zfrep6  5218  funmo  6508  funcnv  6561  fncnv  6565  isarep2  6582  fnres  6619  mptfnf  6627  fnopabg  6629  fvopab3ig  6938  opabex  7171  fnoprabg  7486  ovidi  7506  ovig  7509  caovmo  7600  zfrep6OLD  7904  oprabexd  7924  oprabex  7925  nqerf  10851  cnextfun  24054  perfdvf  25895  taylf  26351  reuxfrdf  32585  abrexdomjm  32602  bj-rep  37433  abrexdom  38104  ralmo  38734  modelaxreplem2  45430