Theorem moanimv 2653

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573

This theorem is referenced by:  2reuswap  3718  2reuswap2  3719  2reu5lem2  3728  2rmoswap  3733  zfrep6  5254  funmo  6553  funcnv  6606  fncnv  6610  isarep2  6626  fnres  6663  mptfnf  6671  fnopabg  6673  fvopab3ig  6986  opabex  7219  fnoprabg  7534  ovidi  7554  ovig  7557  caovmo  7648  zfrep6OLD  7952  oprabexd  7972  oprabex  7973  nqerf  10915  cnextfun  24190  perfdvf  26031  taylf  26490  reuxfrdf  32778  abrexdomjm  32794  bj-rep  37632  abrexdom  38303  ralmo  38933  modelaxreplem2  45614