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

Theorem mobii 2547
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 1909. (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 228 . . 3 (𝜒𝜓)
32moimi 2544 . 2 (∃*𝑥𝜓 → ∃*𝑥𝜒)
41biimpi 216 . . 3 (𝜓𝜒)
54moimi 2544 . 2 (∃*𝑥𝜒 → ∃*𝑥𝜓)
63, 5impbii 209 1 (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 206  ∃*wmo 2537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ex 1779  df-mo 2539
This theorem is referenced by:  eubii  2584  cbvmo  2603  moanmo  2621  2moswapv  2628  2moswap  2643  nulmo  2712  rmobiia  3385  rmoanidOLD  3391  rmov  3510  euxfr2w  3725  euxfr2  3727  rmoan  3744  reuxfrd  3753  2reu5lem2  3761  2rmoswap  3766  dffun9  6594  funopab  6600  funcnv2  6633  funcnv  6634  fun2cnv  6636  fncnv  6638  imadif  6649  fnres  6694  ov3  7597  oprabex3  8003  brdom6disj  10573  grothprim  10875  axaddf  11186  axmulf  11187  reuxfrdf  32511  rmoun  32514  funcnvmpt  32678  rmoeqi  36189  rmoeqbii  36190  nrmo  36412  alrmomorn  38360  cosscnvssid4  38479  dfeldisj4  38722  disjres  38746  tfsconcatlem  43354  euabsneu  47045  rmotru  48728  oppcthin  49112  indthinc  49134  prsthinc  49136
  Copyright terms: Public domain W3C validator