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

Theorem moanimv 2338
 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 1629 . 2
21moanim 2336 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wmo 2281 This theorem is referenced by:  2reuswap  3128  2reu5lem2  3132  funmo  5462  funcnv  5503  fncnv  5507  isarep2  5525  fnres  5553  fnopabg  5560  fvopab3ig  5795  opabex  5956  zfrep6  5960  fnoprabg  6163  oprabexd  6178  oprabex  6179  ovidi  6184  ovig  6187  caovmo  6276  th3qcor  7004  nqerf  8797  cnextfun  18085  perfdvf  19780  taylf  20267  2reuswap2  23965  abrexdomjm  23978  mptfnf  24063  abrexdom  26386  2rmoswap  27893 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
 Copyright terms: Public domain W3C validator