Theorem moanimv 2613

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

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

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 2534

This theorem is referenced by:  2reuswap  3719  2reuswap2  3720  2reu5lem2  3729  2rmoswap  3734  funmo  6533  funmoOLD  6534  funcnv  6587  fncnv  6591  isarep2  6610  fnres  6647  mptfnf  6655  fnopabg  6657  fvopab3ig  6966  opabex  7196  fnoprabg  7514  ovidi  7534  ovig  7537  caovmo  7628  zfrep6  7935  oprabexd  7956  oprabex  7957  nqerf  10889  cnextfun  23957  perfdvf  25810  taylf  26274  reuxfrdf  32426  abrexdomjm  32442  abrexdom  37719  modelaxreplem2  44962