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  3121  rmov  3208  euxfr2  3373  rmoan  3388  2reu5lem2  3396  reuxfr2d  4851  dffun9  5876  funopab  5881  funcnv2  5915  funcnv  5916  fun2cnv  5918  fncnv  5920  imadif  5931  fnres  5965  ov3  6750  oprabex3  7102  brdom6disj  9298  grothprim  9600  axaddf  9910  axmulf  9911  reuxfr3d  29178  funcnvmptOLD  29310  funcnvmpt  29311  2rmoswap  40488
  Copyright terms: Public domain W3C validator