Theorem moanimv 2617

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2618 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 528	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2547	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1928	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2616	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃*wmo 2536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-mo 2538

This theorem is referenced by:  2reuswap  3755  2reuswap2  3756  2reu5lem2  3765  2rmoswap  3770  funmo  6583  funmoOLD  6584  funcnv  6637  fncnv  6641  isarep2  6659  fnres  6696  mptfnf  6704  fnopabg  6706  fvopab3ig  7012  opabex  7240  fnoprabg  7556  ovidi  7576  ovig  7579  caovmo  7670  zfrep6  7978  oprabexd  7999  oprabex  8000  nqerf  10968  cnextfun  24088  perfdvf  25953  taylf  26417  reuxfrdf  32519  abrexdomjm  32535  abrexdom  37717  modelaxreplem2  44944