Theorem moanimv 2645

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

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

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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  2reuswap  3704  2reuswap2  3705  2reu5lem2  3714  2rmoswap  3719  zfrep6  5242  funmo  6547  funcnv  6601  fncnv  6605  isarep2  6621  fnres  6658  mptfnf  6666  fnopabg  6668  fvopab3ig  6981  opabex  7218  fnoprabg  7535  ovidi  7555  ovig  7558  caovmo  7650  zfrep6OLD  7956  oprabexd  7976  oprabex  7977  nqerf  10996  cnextfun  24363  perfdvf  26203  taylf  26670  reuxfrdf  33069  abrexdomjm  33085  bj-rep  37957  abrexdom  38632  ralmo  39260  modelaxreplem2  45921