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

Theorem mobidv 2289
 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:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem mobidv
StepHypRef Expression
1 nfv 1754 . 2
2 mobidv.1 . 2
31, 2mobid 2287 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187  wmo 2267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-12 1907 This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664  df-eu 2270  df-mo 2271 This theorem is referenced by:  mobii  2291  mosubopt  4719  dffun6f  5615  funmo  5617  caovmo  6520  1stconst  6895  2ndconst  6896  brdom3  8954  brdom6disj  8958  imasaddfnlem  15385  imasvscafn  15394  hausflim  20927  hausflf  20943  cnextfun  21010  haustsms  21081  limcmo  22714  perfdvf  22735  phpreu  31633  funressnfv  38020
 Copyright terms: Public domain W3C validator