Theorem moanimv 2707

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2708 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 524	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2617	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 476	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 2029	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2706	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  ∃*wmo 2603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-mo 2605

This theorem is referenced by:  2reuswap  3637  2reu5lem2  3641  funmo  6143  funcnv  6195  fncnv  6199  isarep2  6215  fnres  6244  mptfnf  6252  fnopabg  6254  fvopab3ig  6529  opabex  6744  fnoprabg  7026  ovidi  7044  ovig  7047  caovmo  7136  zfrep6  7401  oprabexd  7420  oprabex  7421  nqerf  10074  cnextfun  22245  perfdvf  24073  taylf  24521  2reuswap2  29877  abrexdomjm  29889  abrexdom  34063  2rmoswap  42003