Theorem moanimv 2619

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

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

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 2539

This theorem is referenced by:  2reuswap  3692  2reuswap2  3693  2reu5lem2  3702  2rmoswap  3707  zfrep6  5224  funmo  6514  funcnv  6567  fncnv  6571  isarep2  6588  fnres  6625  mptfnf  6633  fnopabg  6635  fvopab3ig  6943  opabex  7175  fnoprabg  7490  ovidi  7510  ovig  7513  caovmo  7604  zfrep6OLD  7908  oprabexd  7928  oprabex  7929  nqerf  10853  cnextfun  24029  perfdvf  25870  taylf  26326  reuxfrdf  32560  abrexdomjm  32577  bj-rep  37380  abrexdom  38051  ralmo  38681  modelaxreplem2  45406