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

Theorem mobii 2630
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 2628 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43trud 1642 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1633  ∃*wmo 2608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-tru 1635  df-ex 1854  df-nf 1859  df-eu 2611  df-mo 2612
This theorem is referenced by:  moanmo  2670  2moswap  2685  rmobiia  3271  rmov  3362  euxfr2  3532  rmoan  3547  2reu5lem2  3555  reuxfr2d  5040  dffun9  6078  funopab  6084  funcnv2  6118  funcnv  6119  fun2cnv  6121  fncnv  6123  imadif  6134  fnres  6168  ov3  6963  oprabex3  7323  brdom6disj  9566  grothprim  9868  axaddf  10178  axmulf  10179  reuxfr3d  29658  funcnvmptOLD  29797  funcnvmpt  29798  alrmomorn  34464  cosscnvssid4  34568  2rmoswap  41708
  Copyright terms: Public domain W3C validator