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

Theorem moanimv 2530
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 1840 . 2 𝑥𝜑
21moanim 2528 1 (∃*𝑥(𝜑𝜓) ↔ (𝜑 → ∃*𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  ∃*wmo 2470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-eu 2473  df-mo 2474
This theorem is referenced by:  2reuswap  3397  2reu5lem2  3401  funmo  5873  funcnv  5926  fncnv  5930  isarep2  5946  fnres  5975  mptfnf  5982  fnopabg  5984  fvopab3ig  6245  opabex  6448  fnoprabg  6726  ovidi  6744  ovig  6747  caovmo  6836  zfrep6  7096  oprabexd  7115  oprabex  7116  nqerf  9712  cnextfun  21808  perfdvf  23607  taylf  24053  2reuswap2  29217  abrexdomjm  29233  abrexdom  33196  2rmoswap  40518
  Copyright terms: Public domain W3C validator