Theorem moanimv 2647

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567

This theorem is used by:  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2rmoswap  3722  zfrep6  5246  funmo  6577  funcnv  6634  fncnv  6638  isarep2  6654  fnres  6691  mptfnf  6699  fnopabg  6701  fvopab3ig  7015  opabex  7252  fnoprabg  7569  ovidi  7590  ovig  7593  caovmo  7685  zfrep6OLD  7994  oprabexd  8014  oprabex  8015  nqerf  11045  cnextfun  24416  perfdvf  26256  taylf  26721  reuxfrdf  33162  abrexdomjm  33178  bj-rep  38193  abrexdom  38869  ralmo  39495  modelaxreplem2  46175