Theorem moanimv 2640

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2641 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 532	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2567	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1931	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2639	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃*wmo 2555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2557

This theorem is referenced by:  2reuswap  3660  2reuswap2  3661  2reu5lem2  3670  2rmoswap  3675  funmo  6351  funcnv  6404  fncnv  6408  isarep2  6424  fnres  6457  mptfnf  6466  fnopabg  6468  fvopab3ig  6755  opabex  6974  fnoprabg  7269  ovidi  7288  ovig  7291  caovmo  7381  zfrep6  7660  oprabexd  7680  oprabex  7681  nqerf  10390  cnextfun  22764  perfdvf  24602  taylf  25055  reuxfrdf  30361  abrexdomjm  30374  abrexdom  35448