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

Theorem moanimv 2667
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 1990 . 2 𝑥𝜑
21moanim 2665 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  ∃*wmo 2606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-10 2166  ax-12 2194
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1852  df-nf 1857  df-eu 2609  df-mo 2610
This theorem is referenced by:  2reuswap  3549  2reu5lem2  3553  funmo  6063  funcnv  6117  fncnv  6121  isarep2  6137  fnres  6166  mptfnf  6174  fnopabg  6176  fvopab3ig  6438  opabex  6645  fnoprabg  6924  ovidi  6942  ovig  6945  caovmo  7034  zfrep6  7297  oprabexd  7318  oprabex  7319  nqerf  9942  cnextfun  22067  perfdvf  23864  taylf  24312  2reuswap2  29634  abrexdomjm  29650  abrexdom  33836  2rmoswap  41688
  Copyright terms: Public domain W3C validator