Theorem moanimv 2622

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543

This theorem is referenced by:  2reuswap  3768  2reuswap2  3769  2reu5lem2  3778  2rmoswap  3783  funmo  6593  funmoOLD  6594  funcnv  6647  fncnv  6651  isarep2  6669  fnres  6707  mptfnf  6715  fnopabg  6717  fvopab3ig  7025  opabex  7257  fnoprabg  7573  ovidi  7593  ovig  7596  caovmo  7687  zfrep6  7995  oprabexd  8016  oprabex  8017  nqerf  10999  cnextfun  24093  perfdvf  25958  taylf  26420  reuxfrdf  32519  abrexdomjm  32535  abrexdom  37690