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

Theorem mobidv 2305
Description: Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypothesis
Ref Expression
mobidv.1
Assertion
Ref Expression
mobidv
Distinct variable group:   ,

Proof of Theorem mobidv
StepHypRef Expression
1 nfv 1707 . 2
2 mobidv.1 . 2
31, 2mobid 2303 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  E*wmo 2283
This theorem is referenced by:  mobii  2307  mosubopt  4750  dffun6f  5607  funmo  5609  caovmo  6512  1stconst  6888  2ndconst  6889  brdom3  8927  brdom6disj  8931  imasaddfnlem  14925  imasvscafn  14934  hausflim  20482  hausflf  20498  cnextfun  20564  haustsms  20634  limcmo  22286  perfdvf  22307  funressnfv  32213
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-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator