Theorem moanimv 2647

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567

This theorem is referenced by:  2reuswap  3710  2reuswap2  3711  2reu5lem2  3720  2rmoswap  3725  zfrep6  5251  funmo  6554  funcnv  6607  fncnv  6611  isarep2  6627  fnres  6664  mptfnf  6672  fnopabg  6674  fvopab3ig  6987  opabex  7220  fnoprabg  7535  ovidi  7555  ovig  7558  caovmo  7649  zfrep6OLD  7953  oprabexd  7973  oprabex  7974  nqerf  10916  cnextfun  24202  perfdvf  26043  taylf  26505  reuxfrdf  32818  abrexdomjm  32834  bj-rep  37691  abrexdom  38362  ralmo  38990  modelaxreplem2  45671