NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mobii Unicode version

Theorem mobii 2240
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 10 . . 3
32mobidv 2239 . 2
43trud 1323 1
Colors of variables: wff setvar class
Syntax hints:   wb 176   wtru 1316  wmo 2205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-tru 1319  df-ex 1542  df-nf 1545  df-eu 2208  df-mo 2209
This theorem is referenced by:  moaneu  2263  moanmo  2264  2moswap  2279  2eu1  2284  rmobiia  2801  rmov  2875  euxfr2  3021  rmoan  3034  2reu5lem2  3042  dffun9  5135  funopab  5139  funsn  5147  funcnv2  5155  funcnv  5156  fncnv  5158  imadif  5171  fnres  5199  ov3  5599
  Copyright terms: Public domain W3C validator