New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  mobii GIF 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 (∃*xψ∃*xχ)

Proof of Theorem mobii
StepHypRef Expression
1 mobii.1 . . . 4 (ψχ)
21a1i 10 . . 3 ( ⊤ → (ψχ))
32mobidv 2239 . 2 ( ⊤ → (∃*xψ∃*xχ))
43trud 1323 1 (∃*xψ∃*xχ)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ⊤ wtru 1316  ∃*wmo 2205 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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