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

Theorem mobii 2568
Description: Formula-building rule for the at-most-one quantifier (inference form). (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 mobi 2566 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
2 mobii.1 . 2 (𝜓𝜒)
31, 2mpg 1892 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 197  ∃*wmo 2563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-ex 1875  df-mo 2565
This theorem is referenced by:  moanmo  2654  2moswap  2669  nulmo  2750  rmoanid  3068  rmobiia  3280  rmov  3375  euxfr2  3552  rmoan  3569  2reu5lem2  3577  reuxfr2d  5056  dffun9  6099  funopab  6105  funcnv2  6137  funcnv  6138  fun2cnv  6140  fncnv  6142  imadif  6153  fnres  6187  ov3  6997  oprabex3  7357  brdom6disj  9609  grothprim  9911  axaddf  10221  axmulf  10222  reuxfr3d  29786  funcnvmpt  29920  alrmomorn  34555  cosscnvssid4  34659  euabsneu  41813  2rmoswap  41858
  Copyright terms: Public domain W3C validator