Theorem moanimv 2616

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2617 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 530	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2544	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 484	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1934	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2615	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∃*wmo 2533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535

This theorem is referenced by:  2reuswap  3743  2reuswap2  3744  2reu5lem2  3753  2rmoswap  3758  funmo  6564  funmoOLD  6565  funcnv  6618  fncnv  6622  isarep2  6640  fnres  6678  mptfnf  6686  fnopabg  6688  fvopab3ig  6995  opabex  7222  fnoprabg  7531  ovidi  7551  ovig  7554  caovmo  7644  zfrep6  7941  oprabexd  7962  oprabex  7963  nqerf  10925  cnextfun  23568  perfdvf  25420  taylf  25873  reuxfrdf  31762  abrexdomjm  31775  abrexdom  36646