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

Theorem moanimv 2518
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 1829 . 2 𝑥𝜑
21moanim 2516 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  ∃*wmo 2458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-eu 2461  df-mo 2462
This theorem is referenced by:  2reuswap  3376  2reu5lem2  3380  funmo  5805  funcnv  5857  fncnv  5861  isarep2  5877  fnres  5906  mptfnf  5913  fnopabg  5915  fvopab3ig  6172  opabex  6365  fnoprabg  6636  ovidi  6654  ovig  6657  caovmo  6746  zfrep6  7004  oprabexd  7023  oprabex  7024  nqerf  9608  cnextfun  21625  perfdvf  23417  taylf  23863  2reuswap2  28505  abrexdomjm  28522  abrexdom  32478  2rmoswap  39616
  Copyright terms: Public domain W3C validator