Theorem moanimv 2612

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533

This theorem is referenced by:  2reuswap  3708  2reuswap2  3709  2reu5lem2  3718  2rmoswap  3723  funmo  6502  funcnv  6555  fncnv  6559  isarep2  6576  fnres  6613  mptfnf  6621  fnopabg  6623  fvopab3ig  6930  opabex  7160  fnoprabg  7476  ovidi  7496  ovig  7499  caovmo  7590  zfrep6  7897  oprabexd  7917  oprabex  7918  nqerf  10843  cnextfun  23967  perfdvf  25820  taylf  26284  reuxfrdf  32453  abrexdomjm  32469  abrexdom  37712  modelaxreplem2  44956