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  3720  2reuswap2  3721  2reu5lem2  3730  2rmoswap  3735  funmo  6534  funmoOLD  6535  funcnv  6588  fncnv  6592  isarep2  6611  fnres  6648  mptfnf  6656  fnopabg  6658  fvopab3ig  6967  opabex  7197  fnoprabg  7515  ovidi  7535  ovig  7538  caovmo  7629  zfrep6  7936  oprabexd  7957  oprabex  7958  nqerf  10890  cnextfun  23958  perfdvf  25811  taylf  26275  reuxfrdf  32427  abrexdomjm  32443  abrexdom  37731  modelaxreplem2  44976