Theorem moanimv 2650

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

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

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 2570

This theorem is used by:  2reuswap  3712  2reuswap2  3713  2reu5lem2  3722  2rmoswap  3727  zfrep6  5255  funmo  6559  funcnv  6612  fncnv  6616  isarep2  6632  fnres  6669  mptfnf  6677  fnopabg  6679  fvopab3ig  6992  opabex  7225  fnoprabg  7546  ovidi  7566  ovig  7569  caovmo  7660  zfrep6OLD  7961  oprabexd  7981  oprabex  7982  nqerf  10933  cnextfun  24258  perfdvf  26099  taylf  26561  reuxfrdf  32874  abrexdomjm  32890  bj-rep  37751  abrexdom  38422  ralmo  39050  modelaxreplem2  45729