Theorem moanimv 2620

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

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

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540

This theorem is referenced by:  2reuswap  3693  2reuswap2  3694  2reu5lem2  3703  2rmoswap  3708  zfrep6  5224  funmo  6508  funcnv  6561  fncnv  6565  isarep2  6582  fnres  6619  mptfnf  6627  fnopabg  6629  fvopab3ig  6937  opabex  7168  fnoprabg  7483  ovidi  7503  ovig  7506  caovmo  7597  zfrep6OLD  7901  oprabexd  7921  oprabex  7922  nqerf  10844  cnextfun  24039  perfdvf  25880  taylf  26337  reuxfrdf  32575  abrexdomjm  32592  bj-rep  37396  abrexdom  38065  ralmo  38695  modelaxreplem2  45424