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

Theorem moanimv 2352
Description: Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
moanimv
Distinct variable group:   ,

Proof of Theorem moanimv
StepHypRef Expression
1 nfv 1707 . 2
21moanim 2350 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  E*wmo 2283
This theorem is referenced by:  2reuswap  3302  2reu5lem2  3306  funmo  5609  funcnv  5653  fncnv  5657  isarep2  5673  fnres  5702  fnopabg  5709  fvopab3ig  5953  opabex  6141  fnoprabg  6403  ovidi  6421  ovig  6424  caovmo  6512  zfrep6  6768  oprabexd  6787  oprabex  6788  nqerf  9329  cnextfun  20564  perfdvf  22307  taylf  22756  2reuswap2  27387  abrexdomjm  27405  mptfnf  27499  abrexdom  30221  2rmoswap  32189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator