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

Theorem mobii 2543
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.) Avoid ax-5 1914. (Revised by Wolf Lammen, 24-Sep-2023.)
Hypothesis
Ref Expression
mobii.1 (𝜓𝜒)
Assertion
Ref Expression
mobii (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)

Proof of Theorem mobii
StepHypRef Expression
1 mobii.1 . . . 4 (𝜓𝜒)
21biimpri 227 . . 3 (𝜒𝜓)
32moimi 2540 . 2 (∃*𝑥𝜓 → ∃*𝑥𝜒)
41biimpi 215 . . 3 (𝜓𝜒)
54moimi 2540 . 2 (∃*𝑥𝜒 → ∃*𝑥𝜓)
63, 5impbii 208 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 205  ∃*wmo 2533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-mo 2535
This theorem is referenced by:  eubii  2580  cbvmowOLD  2599  cbvmo  2600  moanmo  2619  2moswapv  2626  2moswap  2641  nulmo  2709  rmobiia  3383  rmoanidOLD  3389  rmov  3502  euxfr2w  3714  euxfr2  3716  rmoan  3733  reuxfrd  3742  2reu5lem2  3750  2rmoswap  3755  dffun9  6569  funopab  6575  funcnv2  6608  funcnv  6609  fun2cnv  6611  fncnv  6613  imadif  6624  fnres  6667  ov3  7557  oprabex3  7951  brdom6disj  10514  grothprim  10816  axaddf  11127  axmulf  11128  reuxfrdf  31696  rmoun  31699  funcnvmpt  31861  nrmo  35200  alrmomorn  37133  cosscnvssid4  37253  dfeldisj4  37496  disjres  37520  tfsconcatlem  41957  euabsneu  45611  rmotru  47329  oppcthin  47499  indthinc  47512  prsthinc  47514
  Copyright terms: Public domain W3C validator