MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moanimv Structured version   Visualization version   GIF version

Theorem moanimv 2619
Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2620 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
StepHypRef Expression
1 ibar 528 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21mobidv 2549 . 2 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑𝜓)))
3 simpl 482 . . 3 ((𝜑𝜓) → 𝜑)
43exlimiv 1930 . 2 (∃𝑥(𝜑𝜓) → 𝜑)
52, 4moanimlem 2618 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  ∃*wmo 2538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540
This theorem is referenced by:  2reuswap  3752  2reuswap2  3753  2reu5lem2  3762  2rmoswap  3767  funmo  6581  funmoOLD  6582  funcnv  6635  fncnv  6639  isarep2  6658  fnres  6695  mptfnf  6703  fnopabg  6705  fvopab3ig  7012  opabex  7240  fnoprabg  7556  ovidi  7576  ovig  7579  caovmo  7670  zfrep6  7979  oprabexd  8000  oprabex  8001  nqerf  10970  cnextfun  24072  perfdvf  25938  taylf  26402  reuxfrdf  32510  abrexdomjm  32526  abrexdom  37737  modelaxreplem2  44996
  Copyright terms: Public domain W3C validator