Theorem moanimv 2611

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∃*wmo 2528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-mo 2530

This theorem is referenced by:  2reuswap  3741  2reuswap2  3742  2reu5lem2  3751  2rmoswap  3756  funmo  6568  funmoOLD  6569  funcnv  6622  fncnv  6626  isarep2  6644  fnres  6682  mptfnf  6690  fnopabg  6692  fvopab3ig  7001  opabex  7232  fnoprabg  7543  ovidi  7564  ovig  7567  caovmo  7658  zfrep6  7958  oprabexd  7979  oprabex  7980  nqerf  10953  cnextfun  23967  perfdvf  25831  taylf  26294  reuxfrdf  32288  abrexdomjm  32301  abrexdom  37203