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

Theorem mobii 2481
 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 2479 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43trud 1484 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195  ⊤wtru 1476  ∃*wmo 2459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463 This theorem is referenced by:  moanmo  2520  2moswap  2535  rmobiia  3109  rmov  3195  euxfr2  3358  rmoan  3373  2reu5lem2  3381  reuxfr2d  4817  dffun9  5832  funopab  5837  funcnv2  5871  funcnv  5872  fun2cnv  5874  fncnv  5876  imadif  5887  fnres  5921  ov3  6695  oprabex3  7048  brdom6disj  9235  grothprim  9535  axaddf  9845  axmulf  9846  reuxfr3d  28713  funcnvmptOLD  28850  funcnvmpt  28851  2rmoswap  39833
 Copyright terms: Public domain W3C validator