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

Theorem moanimv 2519
 Description: Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
moanimv (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem moanimv
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜑
21moanim 2517 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∃*wmo 2459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463 This theorem is referenced by:  2reuswap  3377  2reu5lem2  3381  funmo  5820  funcnv  5872  fncnv  5876  isarep2  5892  fnres  5921  mptfnf  5928  fnopabg  5930  fvopab3ig  6188  opabex  6388  fnoprabg  6659  ovidi  6677  ovig  6680  caovmo  6769  zfrep6  7027  oprabexd  7046  oprabex  7047  nqerf  9631  cnextfun  21678  perfdvf  23473  taylf  23919  2reuswap2  28712  abrexdomjm  28729  abrexdom  32695  2rmoswap  39833
 Copyright terms: Public domain W3C validator