Theorem moanimv 2646

Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2647 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 538	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
2	1	mobidv 2576	. 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓)))
3		simpl 488	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
4	3	exlimiv 1963	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑)
5	2, 4	moanimlem 2645	1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃*wmo 2564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2566

This theorem is used by:  2reuswap  3707  2reuswap2  3708  2reu5lem2  3717  2rmoswap  3722  zfrep6  5248  funmo  6553  funcnv  6606  fncnv  6610  isarep2  6626  fnres  6663  mptfnf  6671  fnopabg  6673  fvopab3ig  6986  opabex  7223  fnoprabg  7540  ovidi  7560  ovig  7563  caovmo  7655  zfrep6OLD  7956  oprabexd  7976  oprabex  7977  nqerf  10943  cnextfun  24296  perfdvf  26137  taylf  26604  reuxfrdf  32974  abrexdomjm  32990  bj-rep  37826  abrexdom  38488  ralmo  39116  modelaxreplem2  45810