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

Theorem mobii 2492
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 2490 . 2 (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
43trud 1490 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wtru 1481  ∃*wmo 2470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-tru 1483  df-ex 1702  df-nf 1707  df-eu 2473  df-mo 2474
This theorem is referenced by:  moanmo  2531  2moswap  2546  rmobiia  3125  rmov  3212  euxfr2  3378  rmoan  3393  2reu5lem2  3401  reuxfr2d  4861  dffun9  5886  funopab  5891  funcnv2  5925  funcnv  5926  fun2cnv  5928  fncnv  5930  imadif  5941  fnres  5975  ov3  6762  oprabex3  7117  brdom6disj  9314  grothprim  9616  axaddf  9926  axmulf  9927  reuxfr3d  29218  funcnvmptOLD  29351  funcnvmpt  29352  2rmoswap  40518
  Copyright terms: Public domain W3C validator