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

Theorem moanimv 2707
Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2708 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 524 . . 3 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
21mobidv 2617 . 2 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑𝜓)))
3 simpl 476 . . 3 ((𝜑𝜓) → 𝜑)
43exlimiv 2029 . 2 (∃𝑥(𝜑𝜓) → 𝜑)
52, 4moanimlem 2706 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  ∃*wmo 2603
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-mo 2605
This theorem is referenced by:  2reuswap  3637  2reu5lem2  3641  funmo  6143  funcnv  6195  fncnv  6199  isarep2  6215  fnres  6244  mptfnf  6252  fnopabg  6254  fvopab3ig  6529  opabex  6744  fnoprabg  7026  ovidi  7044  ovig  7047  caovmo  7136  zfrep6  7401  oprabexd  7420  oprabex  7421  nqerf  10074  cnextfun  22245  perfdvf  24073  taylf  24521  2reuswap2  29877  abrexdomjm  29889  abrexdom  34063  2rmoswap  42003
  Copyright terms: Public domain W3C validator