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

Theorem mobii 2307
 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 2305 . 2
43trud 1404 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184   wtru 1396  E*wmo 2283 This theorem is referenced by:  moanmo  2353  2moswap  2369  2eu1OLD  2377  rmobiia  3048  rmov  3126  euxfr2  3284  rmoan  3298  2reu5lem2  3306  reuxfr2d  4675  dffun9  5621  funopab  5626  funcnv2  5652  funcnv  5653  fun2cnv  5655  fncnv  5657  imadif  5668  fnres  5702  ov3  6439  oprabex3  6789  brdom6disj  8931  grothprim  9233  axaddf  9543  axmulf  9544  reuxfr3d  27388  funcnvmptOLD  27509  funcnvmpt  27510  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-12 1854 This theorem depends on definitions:  df-bi 185  df-tru 1398  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287
 Copyright terms: Public domain W3C validator