Theorem moanimv 2645

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2646 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 536	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2575	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1949	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2644	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∃*wmo 2563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565

This theorem is referenced by:  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2rmoswap  3722  zfrep6  5236  funmo  6531  funcnv  6584  fncnv  6588  isarep2  6605  fnres  6642  mptfnf  6650  fnopabg  6652  fvopab3ig  6965  opabex  7198  fnoprabg  7513  ovidi  7533  ovig  7536  caovmo  7627  zfrep6OLD  7930  oprabexd  7950  oprabex  7951  nqerf  10881  cnextfun  24111  perfdvf  25952  taylf  26411  reuxfrdf  32648  abrexdomjm  32665  bj-rep  37518  abrexdom  38189  ralmo  38819  modelaxreplem2  45515