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

Theorem mobii 2318
 Description: Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
Hypothesis
Ref Expression
mobii.1
Assertion
Ref Expression
mobii

Proof of Theorem mobii
StepHypRef Expression
1 mobii.1 . . . 4
21a1i 11 . . 3
32mobidv 2317 . 2
43trud 1333 1
 Colors of variables: wff set class Syntax hints:   wb 178   wtru 1326  wmo 2283 This theorem is referenced by:  moaneu  2341  moanmo  2342  2moswap  2357  2eu1  2362  rmobiia  2899  rmov  2973  euxfr2  3120  rmoan  3133  2reu5lem2  3141  reuxfr2d  4747  dffun9  5482  funopab  5487  funcnv2  5511  funcnv  5512  fun2cnv  5514  fncnv  5516  imadif  5529  fnres  5562  oprabex3  6189  ov3  6211  brdom6disj  8411  grothprim  8710  axaddf  9021  axmulf  9022  spwmo  14659  reuxfr3d  23977  funcnvmptOLD  24083  funcnvmpt  24084  2rmoswap  27939 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762 This theorem depends on definitions:  df-bi 179  df-tru 1329  df-ex 1552  df-nf 1555  df-eu 2286  df-mo 2287
 Copyright terms: Public domain W3C validator