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

Theorem moanimv 2680
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 1995 . 2 𝑥𝜑
21moanim 2678 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  ∃*wmo 2619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-nf 1858  df-eu 2622  df-mo 2623
This theorem is referenced by:  2reuswap  3562  2reu5lem2  3566  funmo  6047  funcnv  6098  fncnv  6102  isarep2  6118  fnres  6147  mptfnf  6155  fnopabg  6157  fvopab3ig  6420  opabex  6627  fnoprabg  6908  ovidi  6926  ovig  6929  caovmo  7018  zfrep6  7281  oprabexd  7302  oprabex  7303  nqerf  9954  cnextfun  22088  perfdvf  23887  taylf  24335  2reuswap2  29667  abrexdomjm  29683  abrexdom  33857  2rmoswap  41704
  Copyright terms: Public domain W3C validator